×

Uh-oh, it looks like your Internet Explorer is out of date.

For a better shopping experience, please upgrade now.

Mathematical Logic for Computer Science / Edition 2
     

Mathematical Logic for Computer Science / Edition 2

by Mordechai Ben-Ari
 

ISBN-10: 1852333197

ISBN-13: 9781852333195

Pub. Date: 04/27/2001

Publisher: Springer-Verlag New York, LLC

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 a elegant way to teach logic that is both theoretically sound and yet sufficiently elementary for undergraduates. To provide a balanced treatment of

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 computer science students. The method of semantic tableaux provides a 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.

Product Details

ISBN-13:
9781852333195
Publisher:
Springer-Verlag New York, LLC
Publication date:
04/27/2001
Edition description:
2001. Corr. 2nd
Pages:
318
Product dimensions:
0.67(w) x 6.14(h) x 9.21(d)

Table of Contents

Prefacevii
1Introduction1
1.1The origins of mathematical logic1
1.2Propositional calculus2
1.3Predicate calculus3
1.4Theorem proving and logic programming5
1.5Systems of logic6
1.6Exercise7
2Propositional Calculus: Formulas, Models, Tableaux9
2.1Boolean operators9
2.2Propositional formulas12
2.3Interpretations17
2.4Logical equivalence and substitution19
2.5Satisfiability, validity and consequence24
2.6Semantic tableaux29
2.7Soundness and completeness33
2.8Implementation[superscript P]38
2.9Exercises40
3Propositional Calculus: Deductive Systems43
3.1Deductive proofs43
3.2The Gentzen system G45
3.3The Hilbert system H48
3.4Soundness and completeness of H56
3.5A proof checker[superscript P]59
3.6Variant forms of the deductive systems60
3.7Exercises64
4Propositional Calculus: Resolution and BDDs67
4.1Resolution67
4.2Binary decision diagrams (BDDs)81
4.3Algorithms on BDDs88
4.4Complexity95
4.5Exercises99
5Predicate Calculus: Formulas, Models, Tableaux101
5.1Relations and predicates101
5.2Predicate formulas102
5.3Interpretations105
5.4Logical equivalence and substitution107
5.5Semantic tableaux109
5.6Implementation[superscript P]118
5.7Finite and infinite models120
5.8Decidability121
5.9Exercises125
6Predicate Calculus: Deductive Systems127
6.1The Gentzen system G127
6.2The Hilbert system H129
6.3Implementation[superscript P]134
6.4Complete and decidable theories135
6.5Exercises138
7Predicate Calculus: Resolution139
7.1Functions and terms139
7.2Clausal form142
7.3Herbrand models148
7.4Herbrand's Theorem150
7.5Ground resolution152
7.6Substitution153
7.7Unification155
7.8General resolution164
7.9Exercises171
8Logic Programming173
8.1Formulas as programs173
8.2SLD-resolution176
8.3Prolog181
8.4Concurrent logic programming186
8.5Constraint logic programming194
8.6Exercises199
9Programs: Semantics and Verification201
9.1Introduction201
9.2Semantics of programming languages202
9.3The deductive system HL209
9.4Program verification211
9.5Program synthesis213
9.6Soundness and completeness of HL216
9.7Exercises219
10Programs: Formal Specification with Z221
10.1Case study: a traffic signal221
10.2The Z notation224
10.3Case study: semantic tableaux230
10.4Exercises234
11Temporal Logic: Formulas, Models, Tableaux235
11.1Introduction235
11.2Syntax and semantics236
11.3Models of time239
11.4Semantic tableaux242
11.5Implementation of semantic tableaux[superscript P]252
11.6Exercises255
12Temporal Logic: Deduction and Applications257
12.1The deductive system L257
12.2Soundness and completeness of L262
12.3Other temporal logics264
12.4Specification and verification of programs266
12.5Model checking272
12.6Exercises280
ASet Theory283
A.1Finite and infinite sets283
A.2Set operators284
A.3Ordered sets286
A.4Relations and functions287
A.5Cardinality288
A.6Proving properties of sets289
BFurther Reading291
Bibliography293
Index of Symbols297
Index299

Customer Reviews

Average Review:

Post to your social network

     

Most Helpful Customer Reviews

See all customer reviews