| |
| |
List of Figures | |
| |
| |
Preface | |
| |
| |
Acknowledgements | |
| |
| |
| |
Introduction | |
| |
| |
| |
Overview | |
| |
| |
| |
Classical Propositional Logic | |
| |
| |
| |
Syntax | |
| |
| |
| |
Semantics | |
| |
| |
| |
Deduction Systems | |
| |
| |
| |
Hilbert-style Systems | |
| |
| |
| |
Natural Deduction | |
| |
| |
| |
Gentzen Sequents | |
| |
| |
| |
Automated Proof Methods | |
| |
| |
| |
Tableaux | |
| |
| |
| |
Prepositional Resolution | |
| |
| |
| |
The Davis-Putnam Method | |
| |
| |
| |
Binary Decision Diagrams | |
| |
| |
| |
Digressions | |
| |
| |
| |
Expressiveness of Prepositional Classical Logic | |
| |
| |
| |
Boolean Algebras | |
| |
| |
| |
Quantified Prepositional Logic | |
| |
| |
| |
Other Propositional Logics | |
| |
| |
| |
Introduction | |
| |
| |
| |
Constructivity | |
| |
| |
| |
Resources | |
| |
| |
| |
Semantic Paradigms | |
| |
| |
| |
Notation | |
| |
| |
| |
Intuitionistic Logic | |
| |
| |
| |
Intuitionistic Natural Deduction (NJ<sub>0</sub>) | |
| |
| |
| |
Intuitionistic Sequent Calculus (LJ<sub>0</sub>) | |
| |
| |
| |
Relating Sequent Calculus and Natural Deduction | |
| |
| |
| |
Hilbert-style Presentation | |
| |
| |
| |
Normalisation and Cut Elimination | |
| |
| |
| |
Normalisation | |
| |
| |
| |
Cut Elimination | |
| |
| |
| |
Semantics of Intuitionistic Logic | |
| |
| |
| |
Kripke Semantics | |
| |
| |
| |
Intuitionistic Tableaux | |
| |
| |
| |
Functional Interpretation | |
| |
| |
| |
Relating Intuitionistic and Classical Logic | |
| |
| |
| |
Additive and Multiplicative Connectives | |
| |
| |
| |
Linear Logic | |
| |
| |
| |
Syntax of Linear Logic | |
| |
| |
| |
Classical Linear Sequent Calculus | |
| |
| |
| |
Coding Intuitionistic Logic | |
| |
| |
| |
The Curry-Howard Correspondence | |
| |
| |
| |
Introduction | |
| |
| |
| |
Functions | |
| |
| |
| |
Typed �-Calculus and Natural Deduction | |
| |
| |
| |
Typed �-calculus | |
| |
| |
| |
Term Assignment for Natural Deduction | |
| |
| |
| |
Properties | |
| |
| |
| |
Combinatory Logic and Hilbert-Style Axioms | |
| |
| |
| |
Combinatory Logic | |
| |
| |
| |
The Correspondence with Hilbert Axioms | |
| |
| |
| |
Applications of the Curry-Howard Correspondence | |
| |
| |
| |
System F | |
| |
| |
| |
Modal and Temporal Logics | |
| |
| |
| |
Introduction and Motivation | |
| |
| |
| |
S4 and Non-Monotonic Logics | |
| |
| |
| |
Syntax | |
| |
| |
| |
Philosophical Logic and Non-Monotonic Logics | |
| |
| |
| |
Kripke Semantics | |
| |
| |
| |
Decidability | |
| |
| |
| |
Sequent Systems and Tableaux | |
| |
| |
| |
Other Modal Logics Of Interest In Computer Science | |
| |
| |
| |
Hennessy-Milner Logic | |
| |
| |
| |
CTL | |
| |
| |
| |
Propositional Dynamic Logic | |
| |
| |
| |
Model-Checking | |
| |
| |
| |
Sequential Machines and Symbolic Model-Checking | |
| |
| |
| |
Binary Decision Diagrams | |
| |
| |
| |
Developments | |
| |
| |
| |
First-Order Classical Logic | |
| |
| |
| |
Definitions | |
| |
| |
| |
Syntax | |
| |
| |
| |
Semantics | |
| |
| |
| |
Deduction Systems | |
| |
| |
| |
Expressive Power | |
| |
| |
| |
Meta-Mathematical Properties | |
| |
| |
| |
Prenex and Skolem Forms | |
| |
| |
| |
Semantic Herbrand Theory | |
| |
| |
| |
Cut-Elimination and Syntactic Herbrand Theory | |
| |
| |
| |
Digressions | |
| |
| |
| |
Non-classical logics | |
| |
| |
| |
Arithmetic | |
| |
| |
| |
Higher-order logics | |
| |
| |
| |
Resolution | |
| |
| |
| |
Fundamental Ideas | |
| |
| |
| |
Unification | |
| |
| |
| |
Resolution | |
| |
| |
| |
Optimisations | |
| |
| |
| |
Clause Selection Strategies | |
| |
| |
| |
Deletion Strategies | |
| |
| |
| |
Ordering Strategies | |
| |
| |
| |
Semantic Resolution and Set-of-Support Strategies | |
| |
| |
| |
The Linear Strategy | |
| |
| |
| |
Other Refinements of Resolution | |
| |
| |
| |
Resolution as Cut-Only Proofs | |
| |
| |
| |
Tableaux, Connections and Matings | |
| |
| |
| |
First-Order Tableaux | |
| |
| |
| |
Using Herbrand's Theorem | |
| |
| |
| |
Extension Steps | |
| |
| |
| |
Free Variable Tableaux | |
| |
| |
| |
Presentation | |
| |
| |
| |
Herbrandizing On-the-fly | |
| |
| |
| |
Discussion | |
| |
| |
| |
Connections, Matings And Model Elimination | |
| |
| |
| |
Connections and Matings | |
| |
| |
| |
Relation with Resolution | |
| |
| |
| |
Chang's V-Resolution | |
| |
| |
| |
Model Elimination | |
| |
| |
| |
Incorporating Knowledge | |
| |
| |
| |
Motivations | |
| |
| |
| |
Equality and Rewriting | |
| |
| |
| |
Rewriting | |
| |
| |
| |
Paramodulation, or Integrating Rewriting with Resolution | |
| |
| |
| |
Equality and Tableaux | |
| |
| |
| |
Rigid E-Unification | |
| |
| |
| |
Equational Theories | |
| |
| |
| |
Herbrand Theory Modulo an Equational Theory | |
| |
| |
| |
E-Unification | |
| |
| |
| |
Particular Theories | |
| |
| |
| |
Further Reading | |
| |
| |
| |
Other Theories | |
| |
| |
| |
Sorts | |
| |
| |
| |
Theory Resolution | |
| |
| |
| |
Gr�bner Bases | |
| |
| |
| |
Logic Programming Languages | |
| |
| |
| |
Introduction | |
| |
| |
| |
Prolog | |
| |
| |
| |
Constraints | |
| |
| |
| |
Parallelism | |
| |
| |
| |
OR-parallelism | |
| |
| |
| |
AND-parallelism | |
| |
| |
| |
Answers to Exercises | |
| |
| |
| |
Basics of Topology | |
| |
| |
Bibliography | |
| |
| |
Index | |