The Classical Decision Problem

Predicates.- 4.3.4 Encoding the Auxiliary Binary Predicates of NUM*.- 4.4 Historical Remarks.- 5. Other Undecidable Cases.- 5.1 Krom and Horn Formulae.- 5.1.1 Krom Prefix Classes Without Functions or Equality.- 5.1.2 Krom Prefix Classes with Functions or Equality.- 5.2 Few Atomic Subformulae.- 5.2.1 Few Function and Equality Free Atoms.- 5.2.2 Few Equalities and Inequalities.- 5.2.3 Horn Clause Programs With One Krom Rule.- 5.3 Undecidable Logics with Two Variables.- 5.3.1 First-Order Logic with the Choice Operator.- 5.3.2 Two-Variable Logic with Cardinality Comparison.- 5.4 Conjunctions of Prefix-Vocabulary Classes.- 5.4.1 Reduction to the Case of Conjunctions.- 5.4.2 Another Classifiability Theorem.- 5.4.3 Some Results and Open Problems.- 5.5 Historical Remarks.- II. Decidable Classes and Their Complexity.- 6. Standard Classes with the Finite Model Property.- 6.1 Techniques for Proving Complexity Results.- 6.1.1 Domino Problems Revisited.- 6.1.2 Succinct Descriptions of Inputs.- 6.2 The Classical Solvable Cases.- 6.2.1 Monadic Formulae.- 6.2.2 The Bernays-Schönfinkel-Ramsey Class.- 6.2.3 The Gödel-Kalmár-Schütte Class: a Probabilistic Proof.- 6.3 Formulae with One ?.- 6.3.1 A Satisfiability Test for [?*??*, all, all].- 6.3.2 The Ackermann Class.- 6.3.3 The Ackermann Class with Equality.- 6.4 Standard Classes of Modest Complexity.- 6.4.1 The Relational Classes in P, NP and Co-NP.- 6.4.2 Fragments of the Theory of One Unary Function.- 6.4.3 Other Functional Classes.- 6.5 Finite Model Property vs. Infinity Axioms.- 6.6 Historical Remarks.- 7. Monadic Theories and Decidable Standard Classes with Infinity Axioms.- 7.1 Automata, Games and Decidability of Monadic Theories.- 7.1.1 Monadic Theories.- 7.1.2 Automata on Infinite Words and the Monadic Theory of One Successor.- 7.1.3 Tree Automata, Rabin's Theorem and Forgetful De terminacy.- 7.1.4 The Forgetful Determinacy Theorem for Graph Games.- 7.2 The Monadic Second-Order Theory of One Unary Function.- 7.2.1 Decidability Results for One Unary Function.- 7.2.2 The Theory of One Unary Function is not Elementary Recursive.- 7.3 The Shelah Class.- 7.3.1 Algebras with One Unary Operation.- 7.3.2 Canonic Sentences.- 7.3.3 Terminology and Notation.- 7.3.4 1-Satisfiability.- 7.3.5 2-Satisfiability.- 7.3.6 Refinements.- 7.3.7 Villages.- 7.3.8 Contraction.- 7.3.9 Towns.- 7.3.10 The Final Reduction.- 7.4 Historical Remarks.- 8. Other Decidable Cases.- 8.1 First-Order Logic with Two Variables.- 8.2 Unification and Applications to the Decision Problem.- 8.2.1 Unification.- 8.2.2 Herbrand Formulae.- 8.2.3 Positive First-Order Logic.- 8.3 Decidable Classes of Krom Formulae.- 8.3.1 The Chain Criterion.- 8.3.2 The Aanderaa-Lewis Class.- 8.3.3 The Maslov Class.- 8.4 Historical Remarks.- A. Appendix: Tiling Problems.- A.1 Introduction.- A.2 The Origin Constrained Domino Problem.- A.3 Robinson's Aperiodic Tile Set.- A.4 The Unconstrained Domino Problem.- A.5 The Periodic Problem and the Inseparability Result.- Annotated Bibliography.