This book meets the demand for a self-contained and broad-based account of the concepts, the machinery and the use of automated reasoning. The mathematical logic foundations are described in conjunction with practical application, all with the minimum of prerequisites. The approach is constructive, concrete and algorithmic: a key feature is that methods are described with reference to actual implementations (for which code is supplied) that readers can use, modify and experiment with. This book is ideally suited for those seeking a one-stop source for the general area of automated reasoning. It can be used as a reference, or as a place to learn the fundamentals, either in conjunction with advanced courses or for self study.
Author(s): John Harrison
Publisher: Cambdirdge University Press
Year: 2009
Language: English
Pages: 703
Half-title......Page 3
Title......Page 5
Copyright......Page 6
Dedication......Page 7
Contents......Page 9
Preface......Page 13
Ideological orientation......Page 14
What's not in this book......Page 16
Acknowledgements......Page 17
How to read this book......Page 18
The software in this book......Page 19
1.1 What is logical reasoning?......Page 23
1.2 Calculemus!......Page 26
1.3 Symbolism......Page 27
1.4 Boole's algebra of logic......Page 28
Mechanization......Page 30
1.5 Syntax and semantics......Page 31
Abstract and concrete syntax......Page 33
1.6 Symbolic computation and OCaml......Page 35
1.7 Parsing......Page 38
Lexing......Page 39
Parsing......Page 40
1.8 Prettyprinting......Page 43
Further reading......Page 45
Exercises......Page 46
Representation in OCaml......Page 47
Concrete syntax......Page 48
Primitive propositions......Page 50
Syntax operations......Page 52
2.2 The semantics of propositional logic......Page 54
Truth-tables mechanized......Page 56
Formal and natural language......Page 58
2.3 Validity, satisfiability and tautology......Page 61
Tautology and satisfiability checking......Page 62
Substitution......Page 63
Some important tautologies......Page 66
2.4 The De Morgan laws, adequacy and duality......Page 68
Duality......Page 70
2.5 Simplification and negation normal form......Page 71
2.6 Disjunctive and conjunctive normal forms......Page 76
DNF via truth tables......Page 77
DNF via transformation......Page 79
Set-based representation......Page 80
CNF......Page 82
2.7 Applications of propositional logic......Page 83
Ramsey's theorem......Page 84
Digital circuits......Page 85
Addition......Page 87
Multiplication......Page 91
Primality and factorization......Page 93
The power of propositional logic......Page 94
2.8 Definitional CNF......Page 95
Implementation of definitional CNF......Page 97
Optimizations......Page 99
2.9 The Davis-Putnam procedure......Page 101
The 1-literal rule......Page 102
The affirmative–negative rule......Page 103
Rule for eliminating atomic formulas......Page 104
The DPLL procedure......Page 106
Iterative DPLL......Page 108
Backjumping and learning......Page 110
2.10 The Stalmarck's method......Page 112
Triplets......Page 113
Simple rules......Page 114
0-saturation......Page 116
Higher saturation levels......Page 118
Top-level function......Page 120
2.11 Binary decision diagrams......Page 121
Complement edges......Page 122
Implementation......Page 123
Exploiting definitions......Page 127
2.12 Compactness......Page 129
Colouring infinite graphs......Page 131
Further reading......Page 133
Exercises......Page 135
3.1 First-order logic and its implementation......Page 140
Quantifiers......Page 142
3.2 Parsing and printing......Page 144
3.3 The semantics of first-order logic......Page 145
The set of free variables......Page 149
Validity and satisfiability......Page 151
3.4 Syntax operations......Page 152
Substitution in terms......Page 153
Substitution in formulas......Page 155
3.5 Prenex normal form......Page 161
3.6 Skolemization......Page 166
3.7 Canonical models......Page 173
3.8 Mechanizing Herbrand's theorem......Page 180
3.9 Unification......Page 186
A unification algorithm......Page 188
Using unification......Page 193
3.10 Tableaux......Page 195
Tableaux......Page 198
3.11 Resolution......Page 201
Implementation......Page 205
3.12 Subsumption and replacement......Page 207
Linear resolution......Page 216
Positive resolution......Page 218
Semantic resolution......Page 220
The set of support strategy......Page 221
Hyperresolution......Page 223
3.14 Horn clauses and Prolog......Page 224
Implementation......Page 229
Prolog......Page 230
SLD resolution......Page 234
3.15 Model elimination......Page 235
Model elimination and connection tableaux......Page 236
Implementation......Page 241
Search optimization......Page 243
Retrospective: top-down vs. bottom-up......Page 246
3.16 More first-order metatheorems......Page 247
Further reading......Page 250
Exercises......Page 252
4.1 Equality axioms......Page 257
OCaml implementation......Page 261
4.2 Categoricity and elementary equivalence......Page 263
Metatheorems......Page 264
Consequences......Page 266
4.3 Equational logic and completeness theorems......Page 268
Soundness and completeness......Page 269
The difficulty of equational proofs......Page 270
4.4 Congruence closure......Page 271
Implementation of congruence closure......Page 272
Equality decision procedure......Page 274
4.5 Rewriting......Page 276
Canonical rewrite systems......Page 278
Abstract reduction relations......Page 279
Implementing rewriting......Page 284
4.6 Termination orderings......Page 286
Lexicographic path orders......Page 287
Properties of the LPO......Page 290
4.7 Knuth-Bendix completion......Page 293
Critical pairs......Page 295
Completion......Page 299
Interreduction......Page 303
Dealing with commutativity......Page 307
Unfailing completion......Page 308
Predicate formulations......Page 309
Equivalence elimination......Page 310
Brand’s S- and T-modifications......Page 311
Brand’s E-modification......Page 313
Implementation......Page 316
4.9 Paramodulation......Page 319
Refutation completeness of paramodulation......Page 320
Implementation......Page 323
Further reading......Page 325
Exercises......Page 326
5.1 The decision problem......Page 330
5.2 The AE fragment......Page 331
5.3 Miniscoping and the monadic fragment......Page 335
5.4 Syllogisms......Page 339
5.5 The finite model property......Page 342
Instances of the finite model property......Page 346
Decidable and undecidable prefix classes......Page 347
Adding equality......Page 349
5.6 Quantifier elimination......Page 350
Quantifier elimination......Page 352
Example: dense linear orders......Page 355
5.7 Presburger arithmetic......Page 358
Canonical forms......Page 360
Cooper's algorithm......Page 363
Optimizations......Page 371
Natural numbers......Page 372
Skolem arithmetic and other variants......Page 373
Polynomial manipulation......Page 374
Properties of univariate polynomials......Page 377
Quantifier elimination method......Page 378
Polynomial utilities......Page 380
Pseudo-division......Page 381
Sign determination......Page 383
Main algorithm......Page 385
5.9 The real numbers......Page 388
Examples......Page 397
Improvements......Page 400
Word problems......Page 402
Rings......Page 403
The ring of polynomials......Page 405
The word problem for rings......Page 409
The word problem for torsion-free rings......Page 411
The word problem for integral domains......Page 412
Fields......Page 416
The Rabinowitsch trick......Page 417
Algebraically closed fields......Page 419
Abelian monoids and groups......Page 420
5.11 Gröbner bases......Page 422
Polynomial reduction......Page 424
Confluence......Page 426
Gröbner bases......Page 431
Buchberger's algorithm......Page 432
Universal decision procedure......Page 434
5.12 Geometric theorem proving......Page 436
Complex coordinates......Page 439
Degenerate cases......Page 440
Wu's method......Page 441
Examples......Page 444
5.13 Combining decision procedures......Page 447
Limitations......Page 448
Craig's interpolation theorem......Page 449
The Nelson-Oppen method......Page 457
Homogenization......Page 458
Interpolants and stable infiniteness......Page 461
Naive combination algorithm......Page 463
The Nelson–Oppen procedure......Page 467
Convexity......Page 468
Shostak's method......Page 469
Modern SMT systems......Page 471
Further reading......Page 472
Exercises......Page 477
6.1 Human-oriented methods......Page 486
6.2 Interactive provers and proof checkers......Page 488
LCF......Page 489
6.3 Proof systems for first-order logic......Page 491
6.4 LCF implementation of first-order logic......Page 495
6.5 Propositional derived rules......Page 500
Elementary derived rules......Page 501
Derived connectives......Page 505
6.6 Proving tautologies by inference......Page 506
Simulating tableau steps......Page 507
Tableaux by inference......Page 509
Proving tautologies......Page 510
Basic equality properties......Page 511
More quantifier rules......Page 512
Congruence rules for formulas......Page 513
6.8 First-order proof by inference......Page 516
Main tableau code......Page 517
Assigning Skolem functions......Page 521
Eliminating Skolem functions......Page 524
Completeness of first-order logic......Page 526
Tactics......Page 528
Justifications......Page 532
Declarative proof......Page 537
LCF and efficiency......Page 540
Further reading......Page 542
Exercises......Page 544
7.1 Hilbert's programme......Page 548
7.2 Tarski’s theorem on the undefinability of truth......Page 552
Arithmetization of syntax......Page 553
Outline of Tarski's theorem......Page 556
Many things are definable......Page 557
Self-referential sentences......Page 559
The fixpoint lemma......Page 561
Tarski's theorem......Page 562
7.3 Incompleteness of axiom systems......Page 563
7.4 Gödel’s incompleteness theorem......Page 568
…Formulas......Page 569
…Formulas......Page 571
Gödel’s first incompleteness theorem......Page 574
7.5 Definability and decidability......Page 577
Turing machines......Page 578
…Formulas and computability......Page 583
7.6 Church's theorem......Page 586
Robinson arithmetic......Page 587
Evaluation of terms......Page 588
Additional consequences of the Robinson axioms......Page 589
The…......Page 591
Church's theorem......Page 595
Consistency and Hilbert's programme......Page 597
Gödel’s second incompleteness theorem......Page 598
Reflection principles......Page 601
Hilbert's tenth problem......Page 602
The theory of rationals......Page 604
Sharper forms of Church's theorem......Page 605
The Rosser construction......Page 606
Essential undecidability......Page 607
7.8 Retrospective: the nature of logic......Page 608
Further reading......Page 609
Exercises......Page 611
Mathematical notation and terminology......Page 615
Sets......Page 616
Functions......Page 617
Cardinals......Page 619
Inductive definitions......Page 620
Wellfoundedness......Page 623
Functional programming......Page 625
The OCaml toplevel......Page 626
Expressions and definitions......Page 627
Functions......Page 629
Recursive functions......Page 631
Polymorphism and type inference......Page 633
Recursive types and pattern-matching......Page 634
Exceptions......Page 637
Lists......Page 638
Our common OCaml functions......Page 639
General parsing functions......Page 645
Parsing formulas......Page 646
Printing formulas......Page 648
Parsing first-order terms and formulas......Page 650
Printing first-order terms and formulas......Page 651
References......Page 653
Index......Page 690
