In this paper we give an overview of resolution methods for extended propositional modal logics. We adopt the standard translation approach and consider different resolution refinements which provide decision procedures for the resulting clause sets. Our procedures are based on ordered resolution and selection-based resolution. The logics that we cover are multi-modal logics defined over relations closed under intersection, union, converse and possibly complementation.

What precisely are fragments of classical first-order logic showing “modal” behaviour? Perhaps the most influential answer is that of Gabbay 1981, which identifies them with so-called “finite-variable fragments”, using only some fixed finite number of variables (free or bound). This view-point has been endorsed by many authors (cf. van Benthem 1991). We will investigate these fragments, and find that, illuminating and interesting though they are, they lack the required nice behaviour in our sense. (Several new negative results support this claim.) (...) As a counterproposal, then, we define a large fragment of predicate logic characterized by its use of only bounded quantification. This so-called guarded fragment enjoys the above nice properties, including decidability, through an effectively bounded finite model property. (These are new results, obtained by generalizing notions and techniques from modal logic.) Moreover, its own internal finite variable hierarchy turns out to work well. Finally, we shall make another move. The above analogy works both ways. Modal operators are like quantifiers, but quantifiers are also like modal operators. This observation inspires a generalized semantics for first-order predicate logic with accessibility constraints on available assignments (cf. N´emeti 1986, 1992) which moves the earlier quantifier restrictions into the semantics. This provides a fresh look at the landscape of possible predicate logics, including candidates sharing various desirable features with basic modal logic – in particular, its decidability. (shrink)

Reasoning About Knowledge is the first book to provide a general discussion of approaches to reasoning about knowledge and its applications to distributed ...

This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much (...) more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included. (shrink)

For a novice this book is a mathematically-oriented introduction to modal logic, the discipline within mathematical logic studying mathematical models of reasoning which involve various kinds of modal operators. It starts with very fundamental concepts and gradually proceeds to the front line of current research, introducing in full details the modern semantic and algebraic apparatus and covering practically all classical results in the field. It contains both numerous exercises and open problems, and presupposes only minimal knowledge in mathematics. A specialist (...) can use the book as a source of references. Results and methods of many directions in propositional modal logic, from completeness and duality to algorithmic problems, are collected and systematically presented in one volume. (shrink)

The addition of "actually" operators to modal languages allows us to capture important inferential behaviours which cannot be adequately captured in logics formulated in simpler languages. Previous work on modal logics containing "actually" operators has concentrated entirely upon extensions of KT5 and has employed a particular modeltheoretic treatment of them. This paper proves completeness and decidability results for a range of normal and nonnormal but quasi-normal propositional modal logics containing "actually" operators, the weakest of which are conservative extensions of K, (...) using a novel generalisation of the standard semantics. (shrink)

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

This book presents one of the most intellectually challenging aspects of computer related mathematics/logic in a way which should make it accessible to a wider audience. The authors look at different types of reduction to show undecidability, but do so using the novel approach of conversation between three famous mathematicians - sometimes using their own words and sometimes in an adapted form. The authors are of international repute and they provide a modern and authoritative treatment of undecidability with special emphasis (...) on rigorous proofs. Numerous worked examples are included. (shrink)

In this note we show that the classical modal technology of Sahlqvist formulas gives quick proofs of the completeness theorems in [8] (D. Gregory, Completeness and decidability results for some propositional modal logics containing "actually" operators, Journal of Philosophical Logic 30(1): 57-78, 2001) and vastly generalizes them. Moreover, as a corollary, interpolation theorems for the logics considered in [8] are obtained. We then compare Gregory's modal language enriched with an "actually" operator with the work of Arthur Prior now known under (...) the name of hybrid logic. This analysis relates the "actually" axioms to standard hybrid axioms, yields the decidability results in [8], and provides a number of complexity results. Finally, we use a bisimulation argument to show that the hybrid language is strictly more expressive than Gregory's language. (shrink)

In their simplest form, hybrid languages are propositional modal languages which can refer to states. They were introduced by Arthur Prior, the inventor of tense logic, and played an important role in his work: because they make reference to specific times possible, they remove the most serious obstacle to developing modal approaches to temporal representation and reasoning. However very little is known about the computational complexity of hybrid temporal logics.In this paper we analyze the complexity of the satisfiability problem of (...) a number of hybrid temporal logics: the basic hybrid language over transitive trees; nominal Until logic; and referential interval logic. We discuss the effects of including nominals, the @ operator, the somewhere modality E, and the difference operator D. Adding nominals to tense logic leads for several frame-classes to an increase in complexity of the satisfiability problem from PSPACE to EXPTIME. On transitive trees, however, the satisfiability problem for this language can be decided in PSPACE. Along the way we make a detour through hybrid propositional dynamic logic: we establish upper bounds for a number of temporal logics by generalizing results due to Passy and Tinchev [29] and De Giacomo [16]. We conclude with some remarks on the relevance of our results to description logic, and draw attention to the utility of the spypoint technique for proving upper and lower bounds. (shrink)

In this note we show that the classical modal technology of Sahlqvist formulas gives quick proofs of the completeness theorems in [8] (D. Gregory, Completeness and decidability results for some propositional modal logics containing “actually” operators, Journal of Philosophical Logic 30(1): 57–78, 2001) and vastly generalizes them. Moreover, as a corollary, interpolation theorems for the logics considered in [8] are obtained. We then compare Gregory's modal language enriched with an “actually” operator with the work of Arthur Prior now known under (...) the name of hybrid logic. This analysis relates the “actually” axioms to standard hybrid axioms, yields the decidability results in [8], and provides a number of complexity results. Finally, we use a bisimulation argument to show that the hybrid language is strictly more expressive than Gregory's language. (shrink)

This paper, we propose a modal logic satisfying minimal requirements for reasoning about diagrams via collection of sets and relations between them, following Harel's proposal. We first give an axiomatics of such a theory and then provide its Kripke semantics. Then we extend previous works of ours in order to obtain a decision procedure based on tableaux for this logic. Beside soundness and completeness of our tableaux, we manage to define a strategy of rule application ensuring termination by extending the (...) usual loop test of modal logic S4 to whole sub-structures of the model being computed. (shrink)

Guarded fragments of first-order logic were recently introduced by Andreka, van Benthem and Nemeti; they consist of relational first-order formulae whose quantifiers are appropriately relativized by atoms. These fragments are interesting because they extend in a natural way many propositional modal logics, because they have useful model-theoretic properties and especially because they are decidable classes that avoid the usual syntactic restrictions (on the arity of relation symbols, the quantifier pattern or the number of variables) of almost all other known decidable (...) fragments of first-order logic. Here, we investigate the computational complexity of these fragments. We prove that the satisfiability problems for the guarded fragment (GF) and the loosely guarded fragment (LGF) of first-order logic are complete for deterministic double exponential time. For the subfragments that have only a bounded number of variables or only relation symbols of bounded arity, satisfiability is EXPTIME-complete. We further establish a tree model property for both the guarded fragment and the loosely guarded fragment, and give a proof of the finite model property of the guarded fragment. It is also shown that some natural, modest extensions of the guarded fragments are undecidable. (shrink)

We identify the computational complexity of the satisfiability problem for FO 2 , the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite (...) model. Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)

This paper, we propose a modal logic satisfying minimal requirements for reasoning about diagrams via collection of sets and relations between them, following Harel's proposal. We first give an axiomatics of such a theory and then provide its Kripke semantics. Then we extend previous works of ours in order to obtain a decision procedure based on tableaux for this logic. Beside soundness and completeness of our tableaux, we manage to define a strategy of rule application ensuring termination by extending the (...) usual loop test of modal logic S4 to whole sub-structures of the model being computed. (shrink)

We identify the computational complexity of the satisfiability problem for FO 2, the fragment of first-order logic consisting of all relational first-order sentences with at most two distinct variables. Although this fragment was shown to be decidable a long time ago, the computational complexity of its decision problem has not been pinpointed so far. In 1975 Mortimer proved that FO 2 has the finite-model property, which means that if an FO 2 -sentence is satisfiable, then it has a finite model. (...) Moreover, Mortimer showed that every satisfiable FO 2 -sentence has a model whose size is at most doubly exponential in the size of the sentence. In this paper, we improve Mortimer's bound by one exponential and show that every satisfiable FO 2 -sentence has a model whose size is at most exponential in the size of the sentence. As a consequence, we establish that the satisfiability problem for FO 2 is NEXPTIME-complete. (shrink)

The study of the connections between mathematical automata and for mal logic is as old as theoretical computer science itself. In the founding paper of the subject, published in 1936, Turing showed how to describe the behavior of a universal computing machine with a formula of first order predicate logic, and thereby concluded that there is no algorithm for deciding the validity of sentences in this logic. Research on the log ical aspects of the theory of finite-state automata, which is (...) the subject of this book, began in the early 1960's with the work of J. Richard Biichi on monadic second-order logic. Biichi's investigations were extended in several directions. One of these, explored by McNaughton and Papert in their 1971 monograph Counter-free Automata, was the characterization of automata that admit first-order behavioral descriptions, in terms of the semigroup theoretic approach to automata that had recently been developed in the work of Krohn and Rhodes and of Schiitzenberger. In the more than twenty years that have passed since the appearance of McNaughton and Papert's book, the underlying semigroup theory has grown enor mously, permitting a considerable extension of their results. During the same period, however, fundamental investigations in the theory of finite automata by and large fell out of fashion in the theoretical com puter science community, which moved to other concerns. (shrink)

This paper gives an overview on translation methods we have developed for nonclassical logics, in particular for modal logics. Optimized ‘functional’ and semi-functional translation into predicate logic is described. Using normal modal logic as an intermediate logic, other logics can be translated into predicate logic as well. As an example, the translation of modal logic of graded modalities is sketched. In the second part of the paper it is shown how to translate Hilbert axioms into properties of the semantic structure (...) and vice versa., i.e. we can automate important parts of correspondence theory. The exact formalisms and the soundness and completeness proofs can be found in the original papers. (shrink)

The purpose of the present paper is to show that modal propositional logics can be interpreted in a logic based on relational calculus. We consider languages with necessity operators [R], where R is an accessibility relation expression representing an element of the algebra of binary relations with operations −,∪,∩, −1 , ◦. The relational logic is based on relational calculus enriched by operations of weakest prespecification and weakest postspecification introduced in Hoare and He Jifeng and investigated in He Jifeng et (...) al . The logic is an extension of the system introduced in Or lowska and investigated in Buszkowski and Or lowska. (shrink)

We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)