This textbook is specifically tailored to the needs of computer science students. It teaches mathematical logic using tableaux techniques pioneered by Beth and Smullyan. The method of semantic tableaux provides an elegant way to teach logic that is both theoretically sound yet sufficiently elementary for undergraduates. To provide a balanced treatment of logic, tableaux are related to deductive proof systems. The book also discusses application of logic to computer science: logic programming, temporal logic and the Z language for formal specification. For the second edition, the book has been totally rewritten and additional material has been included on binary decision diagrams, constraint logic programming, and model checking.

Contents

Preface
Introduction
Propositional Calculus: Formulas, Models, Tableaux
Propositional Calculus: Deductive Systems
Propositional Calculus: Resolution and BDDs
Predicate Calculus: Formulas, Models, Tableau
Predicate Calculus: Deductive Systems
Predicate Calculus: Resolution
Logic Programming
Programs: Semantics and Verification
Programs: Formal Specification with Z
Temporal Logic: Formulas, Models, Tableaux
Temporal Logic: Deduction and Applications
Appendix A Set Theory
Further Reading
Index