| Summary: | 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.
|
|---|