Book:M. Ben-Ari/Mathematical Logic for Computer Science/Second Edition
Jump to navigation
Jump to search
M. Ben-Ari: Mathematical Logic for Computer Science (2nd Edition)
Published $\text {1993}$, Springer Verlag
- ISBN 1-85233-319-7
Subject Matter
Contents
- Preface
- 1 Introduction
- 1.1 The origins of mathematical logic
- 1.2 Propositional calculus
- 1.3 Predicate calculus
- 1.4 Theorem proving and logic programming
- 1.5 Systems of logic
- 1.6 Exercise
- 2 Propositional Calculus: Formulas, Models, Tableaux
- 2.1 Boolean operators
- 2.2 Propositional formulas
- 2.3 Interpretations
- 2.4 Logical equivalence and substitution
- 2.5 Satisfiability, validity and consequence
- 2.6 Semantic tableaux
- 2.7 Soundness and completeness
- 2.8 Implementation$^P$
- 2.9 Exercises
- 3 Propositional Calculus: Deductive Systems
- 3.1 Deductive proofs
- 3.2 The Gentzen system $\mathcal G$
- 3.3 The Hilbert system $\mathcal H$
- 3.4 Soundness and completeness of $\mathcal H$
- 3.5 A proof checker$^P$
- 3.6 Variant forms of the deductive systems$^*$
- 3.7 Exercises
- 4 Propositional Calculus: Resolution and BDDs
- 4.1 Resolution
- 4.2 Binary decision diagrams (BDDs)
- 4.3 Algorithms on BDDs
- 4.4 Complexity$^*$
- 4.5 Exercises
- 5 Predicate Calculus: Formulas, Models, Tableaux
- 5.1 Relations and predicates
- 5.2 Predicate formulas
- 5.3 Interpretations
- 5.4 Logical equivalence and substitution
- 5.5 Semantic tableaux
- 5.6 Implementation$^P$
- 5.7 Finite and infinite models$^*$
- 5.8 Decidability$^*$
- 5.9 Exercises
- 6 Predicate Calculus: Deductive Systems
- 6.1 The Gentzen system $\mathcal G$
- 6.2 The Hilbert system $\mathcal H$
- 6.3 Implementation$^P$
- 6.4 Complete and decidable theories$^*$
- 6.5 Exercises
- 7 Predicate Calculus: Resolution
- 7.1 Functions and terms
- 7.2 Clausal form
- 7.3 Herbrand models
- 7.4 Herbrand's Theorem$^*$
- 7.5 Ground resolution
- 7.6 Substitution
- 7.7 Unification
- 7.8 General resolution
- 7.9 Exercises
- 8 Logic Programming
- 8.1 Formulas as programs
- 8.2 SLD-resolution
- 8.3 Prolog
- 8.4 Concurrent logic programming$^*$
- 8.5 Constraint logic programming$^*$
- 8.6 Exercises
- 9 Programs: Semantics and Verification
- 9.1 Introduction
- 9.2 Semantics of programming languages
- 9.3 The deductive system $\mathcal{HL}$
- 9.4 Program verification
- 9.5 Program synthesis
- 9.6 Soundness and completeness of $\mathcal{HL}$
- 9.7 Exercises
- 10 Programs: Formal Specification with Z
- 10.1 Case study: a traffic signal
- 10.2 The Z notation
- 10.3 Case study: semantic tableaux
- 10.4 Exercises
- 11 Temporal Logic: Formulas, Models, Tableaux
- 11.1 Introduction
- 11.2 Syntax and semantics
- 11.3 Models of time
- 11.4 Semantic tableaux
- 11.5 Implementation of semantic tableaux$^P$
- 11.6 Exercises
- 12 Temporal Logic: Deduction and Applications
- 12.1 The deductive system $\mathcal L$
- 12.2 Soundness and completeness of $\mathcal L^*$
- 12.3 Other temporal logics$^*$
- 12.4 Specification and verification of programs$^*$
- 12.5 Model checking$^*$
- 12.6 Exercises
- A Set Theory
- A.1 Finite and infinite sets
- A.2 Set operators
- A.3 Ordered sets
- A.4 Relations and functions
- A.5 Cardinality
- A.6 Proving properties of sets
- B Further Reading
- Bibliography
- Index of Symbols
- Index