Mathematical logic for computer science / Mordechai Ben-Ari.

Format:

Book

Author/Creator:

Ben-Ari, M., 1948-

Contributor:

Class of 1932 Fund.

Language:

English

Subjects (All):

Logic, Symbolic and mathematical.

Physical Description:

xiv, 304 pages : illustrations ; 24 cm

Edition:

Second edition.

Place of Publication:

London ; New York : Springer, 2003.

Summary:

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 as well as Prolog source code for algorithms may be found via the Springer London web site: http: //www.springer.co.uk/com pubs/ct mlcs.htm Mordechai Ben-Ari is Associate Professor at the Department of Science Teaching of the Weizmann Institute of Science. He has published textbooks on concurrent programming and programming languages.

Contents:

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

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

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

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

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

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

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

8 Logic Programming 173

8.1 Formulas as programs 173

8.2 SLD-resolution 176

8.4 Concurrent logic programming 186

8.5 Constraint logic programming 194

9 Programs: Semantics and Verification 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

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

11 Temporal Logic: Formulas, Models, Tableaux 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

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

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.

Notes:

2nd printing with corrections 2003.

Includes bibliographical references (pages [293]-295) and indexes.

Local Notes:

Acquired for the Penn Libraries with assistance from the Class of 1932 Fund.

ISBN:

1852333197

OCLC:

53161283