# Book:M. Ben-Ari/Mathematical Logic for Computer Science/Third Edition

## M. Ben-Ari: Mathematical Logic for Computer Science, 3rd ed.

Published $\text {2012}$, Springer

ISBN 1-4471-4128-0

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

Next

In Appendix:

Next