| Description |
1 online resource |
| Series |
Oxford logic guides ; 56 |
|
Oxford logic guides ; 56.
|
| Contents |
Cover -- seriespage -- titlepage -- copyright -- dedication -- Preface -- Acknowledgements -- Contents -- 1 Introduction -- 1.1 The limits of decision -- 1.2 Logic -- 1.3 Computability -- 1.4 Complexity -- I Syntactic restrictions -- 2 Roots -- 2.1 The fragments S, S+, R, and R+ -- 2.2 The classical syllogistic -- 2.3 The relational syllogistic -- 2.4 The extended relational syllogistic -- 2.5 Syllogisms -- 2.6 Relational syllogisms -- 3 Variables -- 3.1 The fragment FO2 -- 3.2 Small substructures for FO2 -- 3.3 Tiling problems -- 3.4 The three-variable fragment |
|
3.5 Lower complexity bounds for FO2 -- 3.6 The monadic fragment -- 3.7 Expressive power -- 4 Guards -- 4.1 The fragment GF -- 4.2 A decision procedure for Sat(GF) -- 4.3 Lower complexity bounds for GF -- 4.4 Resolution theorem proving -- 4.5 Deciding GF by resolution -- 4.6 The finite model property -- 4.7 Expressive power -- 4.8 Refutation-completeness of resolution -- 4.8.1 Ground resolution -- 4.8.2 Resolution for arbitrary clauses -- 5 Prefixes -- 5.1 Quantifier-prefix fragments -- 5.2 Existential before universal -- 5.3 Two undecidable cases -- 5.4 One universal quantifier |
|
5.4.1 One universal quantifier without equality -- 5.4.2 One universal quantifier with equality -- 5.4.3 One trailing existential quantifier -- 5.5 Two universal quantifiers -- 5.5.1 Without equality -- 5.5.2 With equality -- 6 Fluting -- 6.1 The fragment F L -- 6.2 Small models for F L3 -- 6.3 Small models for F L -- 6.4 Large models -- 6.5 Sat(F L) is non-elementary -- II Counting quantifiers -- 7 Counting with one variable -- 7.1 The fragment C1 -- 7.2 Lower complexity bounds for N -- 7.3 Linear equations -- 7.4 Extended-Diophantine equations -- 7.5 Complexity-theoretic consequences |
|
7.6 A decision procedure for Sat(C1) -- 8 Counting with two variables -- 8.1 The fragment C2 -- 8.2 Chromaticity and differentiation -- 8.3 Star-types and profiles -- 8.4 Characterizing profiles -- 8.5 A decision procedure for Sat(C2) -- 8.6 Weak semi-normal form -- 9 Guarded counting -- 9.1 The fragment GC2 -- 9.2 Scores and tallies -- 9.3 Reduction to linear programming -- 9.4 Correctness -- 9.5 A decision procedure for Sat(GC2) -- 9.6 Adding a database -- 9.7 Data complexity -- 10 Omitting graphs -- 10.1 Ontology-based query answering -- 10.2 Query answering for FO2 -- 10.3 Labelled graphs |
|
10.4 Structure graphs -- 10.5 Formula graphs -- 10.6 A procedure for query answering in GC2D -- 10.7 Lower bounds for query answering -- 10.8 Key constraints -- 10.9 A procedure for query answering in GC2DK -- III Semantic constraints -- 11 Modalities -- 11.1 The fragments K(C) and GrK(C) -- 11.2 Decision procedures for Sat(K, C) -- 11.3 Lower complexity bounds for Sat(K,C) -- 11.4 Expressive power -- 11.5 Decision procedures for Sat(GrK,C): part 1 -- 11.6 Decision procedures for Sat(GrK,C): part 2 -- 11.7 Lower complexity bounds for Sat(GrK,C) -- 11.8 Extensions of modal logic |
| 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 |
| Subject |
First-order logic.
|
| Form |
Electronic book
|
| ISBN |
9780191960062 |
|
0191960063 |
|
9780192693891 |
|
0192693891 |
|
