Mathematical logic for computer science

Select an Action

Place Hold(s)
Add to My Lists
Email
Print

Title:

Personal Author:

Ben-Ari, Mordechai

Edition:

2rd ed.

Publication Information:

Berlin : Springer, 2003

Physical Description:

xiv, 304 p. : ill. ; 24 cm.

ISBN:

9781852333195

Subject Term:

Logic, Symbolic and mathematical

Available:*

Library	Item Barcode	Call Number	Material Type	Item Category 1	Status
Searching... PSZ JB	30000010194979	QA9 B364 2003	Open Access Book	Book	Searching... Unknown

This is a mathematics textbook with theorems and proofs. 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. In order to provide a balanced treatment of logic, tableaux are related to deductive proof systems. The book presents various logical systems and contains exercises. Still further, Prolog source code is available on an accompanying Web site. The author is an Associate Professor at the Department of Science Teaching, Weizmann Institute of Science.

Author Notes

Mordechai Ben-Ari is Associate Professor at the Department of Science Teaching of the Weizmann Institute of Science.

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

Available:*

On Order

Summary

Summary

Author Notes

Table of Contents