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

From ProofWiki
Jump to navigation Jump to search

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

Published $\text {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


Next


In Appendix:

Next


Further Editions


Source work progress

Retrieved from "https://proofwiki.org/w/index.php?title=Book:M._Ben-Ari/Mathematical_Logic_for_Computer_Science/Third_Edition&oldid=448552"