Book:M. Ben-Ari/Mathematical Logic for Computer Science/Third Edition
From ProofWiki
M. Ben-Ari: Mathematical Logic for Computer Science, 3rd ed.
Published $2012$, Springer
- ISBN 1-4471-4128-0.
Subject Matter
Contents
- 1 Introduction
- 1.1 The Origins of Mathematical Logic
- 1.2 Propositional Logic
- 1.3 First-Order Logic
- 1.4 Modal and Temporal Logics
- 1.5 Program Verification
- 1.6 Summary
- 1.7 Further Reading
- 1.8 Exercise
- References
- 2 Propositional Logic: Formulas, Models, Tableaux
- 2.1 Propositional Formulas
- 2.2 Interpretations
- 2.3 Logical Equivalence
- 2.4 Sets of Boolean Operators $^*$
- 2.5 Satisfiability, Validity and Consequence
- 2.6 Semantic Tableaux
- 2.7 Soundness and Completeness
- 2.8 Summary
- 2.9 Further Reading
- 2.10 Exercises
- References
- 3 Propositional Logic: Deductive Systems
- 3.1 Why Deductive Proofs?
- 3.2 Gentzen System $\mathscr G$
- 3.3 Hilbert System $\mathscr H$
- 3.4 Derived Rules in $\mathscr H$
- 3.5 Theorems for Other Operators
- 3.6 Soundness and Completeness of $\mathscr H$
- 3.7 Consistency
- 3.8 Strong Completeness and Compactness $^*$
- 3.9 Variant Forms of the Deductive Systems $^*$
- 3.10 Summary
- 3.11 Further Reading
- 3.12 Exercises
- References
- 4 Propositional Logic: Resolution
- 4.1 Conjunctive Normal Form
- 4.2 Clausal Form
- 4.3 Resolution Rule
- 4.4 Soundness and Completeness of Resolution $^*$
- 4.5 Hard Examples for Resolution $^*$
- 4.6 Summary
- 4.7 Further Reading
- 4.8 Exercises
- References
- 5 Propositional Logic: Binary Decision Diagrams
- 5.1 Motivation Through Truth Tables
- 5.2 Definition of Binary Decision Diagrams
- 5.3 Reduced Binary Decision Diagrams
- 5.4 Ordered Binary Decision Diagrams
- 5.5 Applying Operators to BDDs
- 5.6 Restriction and Quantification $^*$
- 5.7 Summary
- 5.8 Further Reading
- 5.9 Exercises
- References
- 6 Propositional Logic: SAT Solvers
- 6.1 Properties of Clausal Form
- 6.2 Davis-Putnam Algorithm
- 6.3 DPLL Algorithm
- 6.4 An Extended Example of the DPLL Algorithm
- 6.5 Improving the DPLL Algorithm
- 6.6 Stochastic Algorithm
- 6.7 Complexity of SAT $^*$
- 6.8 Summary
- 6.9 Further Reading
- 6.10 Exercises
- References
- 7 First-Order Logic: Formulas, Models, Tableaux
- 7.1 Relations and Predicates
- 7.2 Formulas in First-Order Logic
- 7.3 Interpretations
- 7.4 Logical Equivalences
- 7.5 Semantic Tableaux
- 7.6 Soundness and Completeness of Semantic Tableaux
- 7.7 Summary
- 7.8 Further Reading
- 7.9 Exercises
- References
- 8 First-Order Logic: Deductive Systems
- 8.1 Gentzen System $\mathscr G$
- 8.2 Hilbert System $\mathscr H$
- 8.3 Equivalence of $\mathscr H$ and $\mathscr G$
- 8.4 Proofs of Theorems in $\mathscr H$
- 8.5 The C-Rule $^*$
- 8.6 Summary
- 8.7 Further Reading
- 8.8 Exercises
- References
- 9 First-Order Logic: Terms and Normal Forms
- 9.1 First-Order Logic with Functions
- 9.2 PCNF and Clausal Form
- 9.3 Herbrand Models
- 9.4 Herbrand's Theorem $^*$
- 9.5 Summary
- 9.6 Further Reading
- 9.7 Exercises
- References
- 10 First-Order Logic: Resolution
- 10.1 Ground Resolution
- 10.2 Substitution
- 10.3 Unification
- 10.4 General Resolution
- 10.5 Soundness and Completeness of General Resolution $^*$
- 10.6 Summary
- 10.7 Further Reading
- 10.8 Exercises
- References
- 11 First-Order Logic: Logic Programming
- 11.1 From Formulas in Logic to Logic Programming
- 11.2 Horn Clauses and SLD-Resolution
- 11.3 Search Rules in SLD-Resolution
- 11.4 Prolog
- 11.5 Summary
- 11.6 Further Reading
- 11.7 Exercises
- References
- 12 First-Order Logic: Undecidability and Model Theory $^*$
- 12.1 Undecidability of First-Order Logic
- 12.2 Decidable Cases of First-Order Logic
- 12.3 Finite and Infinite Models
- 12.4 Complete and Incomplete Theories
- 12.5 Summary
- 12.6 Further Reading
- 12.7 Exercises
- References
- 13 Temporal Logic: Formulas, Models, Tableaux
- 13.1 Introduction
- 13.2 Syntax and Semantics
- 13.3 Models of Time
- 13.4 Linear Temporal Logic
- 13.5 Semantic Tableaux
- 13.6 Binary Temporal Operators $^*$
- 13.7 Summary
- 13.8 Further Reading
- 13.9 Exercises
- References
- 14 Temporal Logic: A Deductive System
- 14.1 Deductive System $\mathscr L$
- 14.2 Theorems of $\mathscr L$
- 14.3 Soundness and Completeness of $\mathscr L$ $^*$
- 14.4 Axioms for the Binary Temporal Operators $^*$
- 14.5 Summary
- 14.6 Further Reading
- 14.7 Exercises
- References
- 15 Verification of Sequential Programs
- 15.1 Correctness Formulas
- 15.2 Deductive System $\mathscr{HL}$
- 15.3 Program Verification
- 15.4 Program Synthesis
- 15.5 Formal Semantics of Programs $^*$
- 15.6 Soundness and Completeness of $\mathscr{HL}$ $^*$
- 15.7 Summary
- 15.8 Further Reading
- 15.9 Exercises
- References
- 16 Verification of Concurrent Programs
- 16.1 Definition of Concurrent Programs
- 16.2 Formalization of Correctness
- 16.3 Deductive Verification of Concurrent Programs
- 16.4 Programs as Automata
- 16.5 Model Checking of Invariance Properties
- 16.6 Model Checking of Liveness Properties
- 16.7 Expressing an LTL Formula as an Automaton
- 16.8 Model Checking Using the Synchronous Automaton
- 16.9 Branching-Time Temporal Logic $^*$
- 16.10 Symbolic Model Checking $^*$
- 16.11 Summary
- 16.12 Further Reading
- 16.13 Exercises
- References
- Appendix Set Theory
- A.1 Finite and Infinite Sets
- A.2 Set Operators
- A.3 Sequences
- A.4 Relations and Functions
- A.5 Cardinality
- A.6 Proving Properties of Sets
- References
- Index of Symbols
- Name Index
- Subject Index