Mathematical Logic for Computer Science

by Mordechai Ben-Ari

Overview

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 students of computer science. The method of semantic tableaux provides an elegant way to teach logic that is both theoretically sound and easy to understand. The uniform use of tableaux-based techniques facilitates learning advanced logical systems based on what the student has learned from elementary systems.

The logical systems presented are: propositional logic, first-order logic, resolution and its application to logic programming, Hoare logic for the verification of sequential programs, and linear temporal logic
for the verification of concurrent programs.

The third edition has been entirely rewritten and includes new chapters on central topics of modern computer science: SAT solvers and model checking.

Product Details

ISBN-13:	9781447141297
Publisher:	Springer-Verlag New York, LLC
Publication date:	06/16/2012
Sold by:	Barnes & Noble
Format:	eBook
File size:	6 MB

About the Author

Mordechai (Moti) Ben-Ari is with the Department of Science Teaching at the Weizmann Institute of Science. He is a Distinguished Educator of the ACM and has received the ACM/SIGCSE Award for Outstanding Contributions to Computer Science Education.

Table of Contents

	Preface	vii
1	Introduction	1
1.1	The origins of mathematical logic	1
1.2	Propositional calculus	2
1.3	Predicate calculus	3
1.4	Theorem proving and logic programming	5
1.5	Systems of logic	6
1.6	Exercise	7
2	Propositional Calculus: Formulas, Models, Tableaux	9
2.1	Boolean operators	9
2.2	Propositional formulas	12
2.3	Interpretations	17
2.4	Logical equivalence and substitution	19
2.5	Satisfiability, validity and consequence	24
2.6	Semantic tableaux	29
2.7	Soundness and completeness	33
2.8	Implementation[superscript P]	38
2.9	Exercises	40
3	Propositional Calculus: Deductive Systems	43
3.1	Deductive proofs	43
3.2	The Gentzen system G	45
3.3	The Hilbert system H	48
3.4	Soundness and completeness of H	56
3.5	A proof checker[superscript P]	59
3.6	Variant forms of the deductive systems	60
3.7	Exercises	64
4	Propositional Calculus: Resolution and BDDs	67
4.1	Resolution	67
4.2	Binary decision diagrams (BDDs)	81
4.3	Algorithms on BDDs	88
4.4	Complexity	95
4.5	Exercises	99
5	Predicate Calculus: Formulas, Models, Tableaux	101
5.1	Relations and predicates	101
5.2	Predicate formulas	102
5.3	Interpretations	105
5.4	Logical equivalence and substitution	107
5.5	Semantic tableaux	109
5.6	Implementation[superscript P]	118
5.7	Finite and infinite models	120
5.8	Decidability	121
5.9	Exercises	125
6	Predicate Calculus: Deductive Systems	127
6.1	The Gentzen system G	127
6.2	The Hilbert system H	129
6.3	Implementation[superscript P]	134
6.4	Complete and decidable theories	135
6.5	Exercises	138
7	Predicate Calculus: Resolution	139
7.1	Functions and terms	139
7.2	Clausal form	142
7.3	Herbrand models	148
7.4	Herbrand's Theorem	150
7.5	Ground resolution	152
7.6	Substitution	153
7.7	Unification	155
7.8	General resolution	164
7.9	Exercises	171
8	Logic Programming	173
8.1	Formulas as programs	173
8.2	SLD-resolution	176
8.3	Prolog	181
8.4	Concurrent logic programming	186
8.5	Constraint logic programming	194
8.6	Exercises	199
9	Programs: Semantics and Verification	201
9.1	Introduction	201
9.2	Semantics of programming languages	202
9.3	The deductive system HL	209
9.4	Program verification	211
9.5	Program synthesis	213
9.6	Soundness and completeness of HL	216
9.7	Exercises	219
10	Programs: Formal Specification with Z	221
10.1	Case study: a traffic signal	221
10.2	The Z notation	224
10.3	Case study: semantic tableaux	230
10.4	Exercises	234
11	Temporal Logic: Formulas, Models, Tableaux	235
11.1	Introduction	235
11.2	Syntax and semantics	236
11.3	Models of time	239
11.4	Semantic tableaux	242
11.5	Implementation of semantic tableaux[superscript P]	252
11.6	Exercises	255
12	Temporal Logic: Deduction and Applications	257
12.1	The deductive system L	257
12.2	Soundness and completeness of L	262
12.3	Other temporal logics	264
12.4	Specification and verification of programs	266
12.5	Model checking	272
12.6	Exercises	280
A	Set Theory	283
A.1	Finite and infinite sets	283
A.2	Set operators	284
A.3	Ordered sets	286
A.4	Relations and functions	287
A.5	Cardinality	288
A.6	Proving properties of sets	289
B	Further Reading	291
	Bibliography	293
	Index of Symbols	297
	Index	299

Editorial Reviews

A textbook for undergraduate students of computer science, explaining mathematical logic as it is used in computer science, rather than, like most texts and courses, as it relates to higher mathematics. Assumes a year or two of basic computer science, but no mathematics beyond set theory, which is outlined in an appendix. Annotation c. Book News, Inc., Portland, OR (booknews.com)

Booknews

Asst. Prof. Manoj Raut, Dhirubhai Ambani Institute of Information and Communication Technology, India

Excerpts from full review posted Jan 15 2013 to Computing Reviews [Review #: CR140831]

I have used the second edition of this book for my class. I find this new third edition more interesting and more elaborately written; I like it very much, and applaud the author for his work.

From the Publisher