Ben-Ari Mathematical Logic for Computer Science

2. Auflage 2001
ISBN: 978-1-4471-0335-6
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, 304 Seiten, eBook

Mathematical Logic for Computer Science is a mathematics textbook with theorems and proofs, but the choice of topics has been guided by the needs of computer science students. The method of semantic tableaux provides an elegant way to teach logic that is both theoretically sound and yet sufficiently elementary for undergraduates. To provide a balanced treatment of logic, tableaux are related to deductive proof systems.

The logical systems presented are:

- Propositional calculus (including binary decision diagrams);

- Predicate calculus;

- Resolution;

- Hoare logic;

- Z;

- Temporal logic.

Answers to exercises (for instructors only) as well as Prolog source code for algorithms may be found via the Springer London web site: http://www.springer.com/978-1-85233-319-5  
Mordechai Ben-Ari is an associate professor in the Department of Science Teaching of the Weizmann Institute of Science. He is the author of numerous textbooks on concurrency,programming languages and logic, and has developed software tools for teaching concurrency. In 2004, Ben-Ari received the ACM/SIGCSE Award for Outstanding Contributions to Computer Science Education.

Zielgruppe

Lower undergraduate

Autoren/Hrsg.

Ben-Ari, Mordechai

Inhaltsverzeichnis

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 Interpretation.- 2.4 Logical equivalence and Substitution.- 2.5 Satisfiability, validity and consequence.- 2.6 Semantic tableaux.- 2.7 Soundness and completeness.- 2.8 Implementationp.- 2.9 Exercises.- 3 Propositional Calculus: Deductive Systems.- 3.1 Deductive proofs.- 3.2 The Gentzen System G.- 3.3 The Hubert System H.- 3.4 Soundness and completeness of H.- 3.5 A proof checkerp.- 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.2Predicate formulas.- 5.3 Interpretation.- 5.4 Logical equivalence and Substitution.- 5.5 Semantic tableaux.- 5.6 Implementationp.- 5.7 Finite and infinite modeis*.- 5.8 Decidability*.- 5.9 Exercises.- 6 Predicate Calculus: Deductive Systems.- 6.1 The Gentzen system G.- 6.2 The Hubert system H.- 6.3 Implementationp.- 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 modeis.- 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 HL.- 9.4 Program verification.- 9.5 Program synthesis.- 9.6 Soundness and completeness of HL.- 9.7 Exercises.- 10 Programs: Formal Specification with Z.- 10.1 Case study: a traflfic 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 oftime.- 11.4 Semantic tableaux.- 11.5 Implementation of semantic tableauxp.- 11.6 Exercises.- 12 Temporal Logic: Deduction and Applications.- 12.1 The deductive system L.- 12.2 Soundness and completeness of L*.- 12.3 Other temporal logics*.- 12.4 Specification and verification of programs*.- 12.5 Model checking*.- 12.6 Exercises.- A Set Theory.- B Further Reading.- Index of Symbols.