摘要:

The question of axiomatizability of first-order temporal logics is studied w.r.t. different semantics and several restrictions on the language. The validity problem for logics admitting flexible interpretations of the predicate symbols or allowing at least binary predicate symbols is shown to be Π11-complete. In contrast, it is decidable for temporal logics with rigid monadic predicate symbols but without function symbols and identity.

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510779

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor

摘要:

Many temporal and modal logic languages can be regarded as subsets of first order logic, i.e. the semantics of a temporal logic formula is given as a first order condition on points of the underlying models (Kripke structures). Often the set of possible models is restricted to models which are trees. A temporal logic language is (first order) expressively complete, if for every first order condition for a node of a tree there exists an equivalent temporal formula which expresses the same condition. In this paper expressive completeness of the temporal logic language with the set of operatorsU(until),S(since), andXk(k-next) is proved, and the result is extended to various other tree-like structures.

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510780

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor

摘要:

In this paper we present a new semantic approach for propositional linear temporal logic with discrete time, strongly based in the well-order of IN (the set of natural numbers). We consider temporal connectives which express precedence, posteriority and simultaneity, and they provide a family of expressively complete temporal logics. The selection of the new semantics and connectives used in this work was principally to obtain a suitable executable temporal logic, which can be used for the specification and control of process behaviour in discrete time in a similar way to thai presented by D. Gabbay in [GAB 89], Our new approach has two advantages: firstly, the connectives are defined intuitively so that they have interpretations which relate to properties of interest in real systems; secondly, it provides a new semantics that facilitates simpler proofs of many valid formulas and metatheorems. To confirm this second advantage, we use our semantics to give a formal proof of the Separation Theorem for one of these logics (specifically LN3). The great interest of this Separation Theorem for the executable temporal logic is emphasised by D. Gabbay in [GAB 89], [GAB 88].

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510781

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor

摘要:

We introduce a two-dimensional temporal logic as a formalism which enables the description of both the history of a world and the evolution of an observer's views about the history. We apply such formalism to the description of certain problems that occur in historical database systems due to updates. The historical dimension describes the history of a world according to an observer's view at a certain moment in time. The transaction dimension describes the evolution of an observer's view; changes can occur in the observer's view of the present and future as well as in his views of the past. The database is seens as an observer of the history of the world. Besides describing the history of the world, the database system can also execute temporal specifications in the form of temporal actions. The two-dimensional formalism is used to describe the effects of updates in the execution of temporal actions. The detection of some problematic effects and its implementation are discussed.

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510782

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor

摘要:

In this work we argue for relevant logics as a basis for paraconsistent epistemic logics. In order to do so, a paraconsistent nonmonotonic multi-agent epistemic logic,MDR(for Modal Defeasible Relevant), is briefly introduced. InMDReach agent has two kinds of belief: an absolute belief that P, represented by AiP, and a defeasible belief that P, represented by DiP. Therefore, an agent can reason with his own absolute and defeasible beliefs about the world and also reason about his beliefs about other agents' beliefs both absolute and defeasible. A theorem is presented showing some patterns of reasoning inMDR. Avron's relevant logicRMI→ s compared proof theoretically with Anderson and Belnap's relevant logicsRandRMand also with Da Costa's paraconsistent logic CI, with respect to some desired properties of absolute and defeasible beliefs. Then we can understand whyRMIwas chosen to be the underlying logic for the monotonie part (the absolute beliefs) ofMDR, and had to be modified and integrated with a nonmonotonic logic in order to be the underlying logic for the nonmonotonic part (defeasible beliefs).

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510783

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510784

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor

摘要:

The instructions put together below fall into three categories. The editor of the review would be grateful to authors for respecting these indications. At times, the length of this summary may attain a dozen lines. It is to be written in size 9 italic Times. An abstract in French will be joined.

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510786

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510787

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510788

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1992.10510789

出版商:Taylor & Francis Group    

年代:1992

数据来源: Taylor