Search

We define the classical syllogistic, together with its extensions by either noun-level negation or transitive verbs, showing that the satisfiability problem for all three fragments is NLogSpace-complete. We show, however, that the satisfiability problem for the extension with both these features is ExpTime-complete. We go on to establish that the Aristotelian syllogisms---together with some auxiliary rules---constitute a sound and complete proof system for the classical syllogistic and its extension by noun-level negation. We exhibit a set of syllogism-like rules that is sound and refutation-complete for the extension by transitive verbs, and show that there is no such system which is sound and complete for this fragment. Finally, we show that, for the extension by both noun-level negation and transitive verbs, there is no system of syllogism-like rules that is even sound and refutation-complete.

A sentence of first-order logic is satisfiable if it is true in some structure, and finitely satisfiable if it is true in some finite structure. For which fragments of first-order logic is there an effective method for determining satisfiability or finite satisfiability? Furthermore, if these problems are decidable for a particular fragment, what is their computational complexity? This book provides an up-to-date survey of the principal axes of research into these questions. Part I focusses on fragments defined by restricting the set of available formulas. Starting with the Aristotelian syllogistic and its relatives, we proceed to consider the two-variable fragment, the guarded fragment, the quantifier-prefix fragments and the fluted fragment. Part II investigates logics with counting quantifiers. We begin with De Morgan’s numerical generalization of the Aristotelian syllogistic, before giving a detailed treatment of the two-variable fragment with counting quantifiers and its guarded subfragment, explaining the application of the latter to ontology-based query answering. Part III concerns logics characterized by semantic constraints, limiting the available interpretations of certain predicates. The origins of this idea lie in propositional modal logic, and therefore we start with a survey of modal and graded modal logics. We then investigate two-variable first-order logic in which certain distinguished binary predicates are interpreted as equivalence relations or transitive relations, extending these results to incorporate counting quantifiers. We finish, slightly breaching the bounds of first-order logic proper, with a chapter on logics interpreted over trees.

We consider fragments of first-order logic (with and without equality) defined by means of standard quantifier prefix specifiers, over signatures containing no function symbols. We determine, in each case, the decidability and complexity of the (finite) satisfiability problem. Two of these results tower above the others. The first concerns the so-called Gödel fragment, where the quantifier prefix features two adjacent universal quantifiers and at least one trailing existential quantifier, but where equality is not allowed. We show that this fragment has the finite model property, and that its satisfiability problem is NExpTime-complete. The second concerns the so-called Goldfarb fragment, which adds equality to the Gödel fragment. We show that the satisfiability and finite satisfiability problems for this fragment are undecidable. We also discuss the effect on lower complexity bounds of making individual constants unavailable.

We consider the so-called fluted fragment, a fragment of first-order logic originating in the work of W.V.O. Quine in which, roughly speaking, the order of quantification of variables is constrained to match the order of occurrence of those variables in atomic formulas. We show that this fragment has the finite model property, and that its satisfiability problem is decidable, but with non-elementary complexity. We also determine, within certain bounds, the complexity of satisfiability for the k-variable subfragment, for all k.

We consider the two-variable fragment of first-order logic with counting quantifiers, but where k distinguished binary predicates are constrained to be interpreted as equivalence relations. We show that, if k=1, the satisfiability and finite satisfiability problems for the resulting logic remain NExpTime-complete. Our treatment here employs the full power of the results on integer linear programming obtained in Chapter 7. In addition, we show that, if k=2, the satisfiability and finite satisfiability problems for the resulting logic become undecidable.

This chapter introduces the notion of counting quantifiers, and presents some fundamental results in the theory of integer linear programming. We explain the notion of the minimal basis of an integer linear programming instance, and obtain bounds on the values occurring in it. We also introduce the notion of the footprint of a solution, and obtain an upper bound on its cardinality. These results will be used throughout the remainder of the book. In the present chapter, they enable us to show that the one-variable fragment of first-order logic with counting quantifiers has the finite model property, and that its satisfiability problem is in NPTime. We additionally consider the numerical syllogistic, a subfragment of the one-variable fragment with counting quantifiers, originally investigated by A. De Morgan. We show that its satisfiability problem is NPTime-hard.

We introduce and motivate the subject of this book, namely, the study of the satisfiability and finite satisfiability problems for various fragments of first-order logic. In addition, we survey the basic results in model theory, computability theory and complexity theory assumed in the sequel, and establish terminology and notation.

We consider the guarded two-variable fragment of first-order logic with counting quantifiers, a subfragment of the two-variable fragment with counting quantifiers in which, in addition to the requirement of guarding, individual constants do not appear. We show that this logic lacks the finite model property, but that its satisfiability and finite satisfiability problems are both nevertheless ExpTime-complete. We introduce the concepts of database and data complexity, and show that the satisfiability and finite satisfiability problems for the guarded two-variable fragment of first-order logic with counting quantifiers and databases remain in ExpTime, and are NPTime-complete for data-complexity.

We introduce the concepts of conjunctive query and (finite) query answering, and show that the problems of query answering and finite query answering in the guarded two-variable fragment of first-order logic with counting quantifiers and databases are in 2-ExpTime, falling to co-NPTime for data complexity. We also consider the extension of this fragment with key constraints, and show that the complexity of the (finite) satisfiability and (finite) query-answering problems does not increase.

We consider the guarded fragment of first-order logic together with its k-variable subfragments. Using the technique of resolution theorem proving, we show that the satisfiability problem for the guarded fragment is in 2-ExpTime, falling to ExpTime if the number of variables is bounded. We obtain matching lower bounds by reduction to the bounded halting problem for alternating Turing machines. We also show that the guarded fragment has the finite model property, and obtain a semantic characterization of its expressive power. An appendix to the chapter provides a proof of the refutation-completeness of resolution-theorem proving with atom orderings and selection functions.

We consider the two-variable fragment of first-order logic, showing that it has the finite model property, and that its satisfiability problem is in NExpTime. We introduce the technique of reduction to the infinite tiling problem, and use it to show that the satisfiability and finite satisfiability problems for the three-variable fragment of first-order logic are both undecidable. We then introduce the technique of reduction to bounded tiling problems and use it to show that the satisfiability problem for the two-variable fragment of first-order logic is NExpTime-hard. We also consider the monadic fragment of first-order logic, and show that its satisfiability problem is also NExpTime-complete. Finally we obtain a semantic characterization of the expressive power of the k-variable fragment of first-order logic.

We consider the two-variable fragment of first-order logic with counting quantifiers. We show that this logic lacks the finite model property, but that its satisfiability and finite satisfiability problems are both nevertheless in NExpTime. Our proof employs the results on integer linear programming obtained in the previous chapter. We also establish parametrized complexity bounds concerning the satisfiability problem for the two-variable fragment with counting quantifiers.

We consider the two-variable fragment of first-order logic, but where k distinguished binary predicates are constrained to be interpreted as equivalence relations. We show that, if k=1, the resulting logic has the finite model property, and that the satisfiability problem remains NExpTime-complete. We further show that, if k=2, the resulting logic loses the finite model property, and that the satisfiability and finite satisfiability problems become 2-NExpTime-complete. Finally, we show that, if k=3, the satisfiability and finite satisfiability problems for the resulting logic become undecidable.

We consider the two-variable fragment of first-order logic with counting quantifiers, but where k distinguished binary predicates are constrained to be interpreted as equivalence relations. We show that, if k=1, the satisfiability and finite satisfiability problems for the resulting logic remain NExpTime-complete. Our treatment here employs the full power of the results on integer linear programming obtained in Chapter 7. In addition, we show that, if k=2, the satisfiability and finite satisfiability problems for the resulting logic become undecidable.