摘要:

To more efficiently cover a wide spectrum of conceptual modeling applications such as computer-aided design, computer-aided manufacturing, and medical information systems, we envision multi-paradigm design environments which have reasoning capability to support analyzing specifcations for correctness. For such applications, information system designers employ conceptual models characterized by semantically-rich specification languages. The problem of providing a comprehensive formal framework for such languages has not been adequately addressed. This paper investigates a formal system for this purpose called Event-Formula Logic (EFL). The analysis focuses in particular on characterizing correctness of database updates. Its applicability is demonstrated from two perspectives: deriving preconditions that guarantee a given update will not violate an integrity constraint, and determining alternative integrity maintenance rules for performing corrective actions when the application semantics requires this update interpretation. The work described in this paper represents an important step in the analysis of database update semantics through the use of algorithmic logic. As a result, it contributes towards providing a formal basis for semantically-rich information system design environments.

ISSN:1166-3081    

DOI:10.1080/11663081.1998.10510942

出版商:Taylor & Francis Group    

年代:1998

数据来源: Taylor

摘要:

In his paper “On Having Bad Contractions, Or: No Room for Recovery” [Te97], N. Tennant attacks the AGM research program of belief revision. We show that he misrepresents the state of affairs in this field of research.

ISSN:1166-3081    

DOI:10.1080/11663081.1998.10510943

出版商:Taylor & Francis Group    

年代:1998

数据来源: Taylor

摘要:

In this paper we define two logics, KLn and BLn, and present tableau-based decision procedures for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of linear discrete temporal logic, it contains a set of unary modal connectives for representing the knowledge possessed by agents. The logic BLn is somewhat similar; it is a temporal logic that contains connectives for representing the beliefs of agents. In addition to a complete formal definition of the two logics and their decision procedures, the paper includes a brief review of their applications in AI and mainstream computer science, correctness proofs for the decision procedures, a number of worked examples illustrating the decision procedures, and some pointers to further work.

ISSN:1166-3081    

DOI:10.1080/11663081.1998.10510944

出版商:Taylor & Francis Group    

年代:1998

数据来源: Taylor

摘要:

A spatial logic is a modal logic of which the models are the mathematical models of space. Successively considering the mathematical models of space that are the incidence geometry and the projective geometry, we will successively establish the language, the semantical basis, the axiomatical presentation, the proof of the decidability and the proof of the completeness of INC, the modal multilogic of incidence geometry, and PRO, the modal multilogic of projective geometry.

ISSN:1166-3081    

DOI:10.1080/11663081.1998.10510945

出版商:Taylor & Francis Group    

年代:1998

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1998.10510946

出版商:Taylor & Francis Group    

年代:1998

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1998.10510941

出版商:Taylor & Francis Group    

年代:1998

数据来源: Taylor