Handbook of Practical Logic and Automated Reasoning

Description

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. 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