| |
| |
| 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 | |