Part I History
Chapter 1 THE EARLY HISTORY OF AUTOMATED DEDUCTION ............. 3
Martin Davis
1 Presburger's Procedure ....................................... 5
2 Newell, Shaw & Simon, and H. Gelernter ....................... 6
3 First-Order Logic ............................................ 7
Bibliography ................................................ 12
Index ....................................................... 15
Part II Classical Logic
Chapter 2 RESOLUTION THEOREM PROVING .......................... 19
Leo Bachmair and Harald Ganzinger
1 Introduction ................................................ 21
2 Preliminaries ............................................... 22
3 Standard Resolution ......................................... 28
4 A Framework for Saturation-Based Theorem Proving ............ 34
5 General Resolution .......................................... 46
6 Basic Resolution Strategies ................................. 59
7 Refined Techniques for Defining Orderings and Selection
Functions ................................................... 66
8 Global Theorem Proving Methods .............................. 84
9 First-Order Resolution Methods .............................. 89
10 Effective Saturation of First-Order Theories ................ 91
11 Concluding Remarks .......................................... 93
Bibliography ................................................ 94
Index ....................................................... 98
Chapter 3 TABLEAUX AND RELATED METHODS ....................... 101
Reiner Hähnle
1 Introduction ............................................... 103
2 Preliminaries .............................................. 104
3 The Tableau Method ......................................... 107
4 Clause Tableaux ............................................ 125
5 Tableaux as a Framework .................................... 152
6 Comparing Calculi .......................................... 164
7 Historical Remarks & Resources ............................. 167
Bibliography ............................................... 168
Notation ................................................... 176
Index ...................................................... 177
Chapter 4 THE INVERSE METHOD ................................. 179
Anatoli Degtyarev and Andrei Voronkov
1 Introduction ............................................... 181
2 Preliminaries .............................................. 185
3 Cooking classical logic .................................... 186
4 Applying the recipe to nonclassical logics ................. 209
5 Naming and connections with resolution ..................... 219
6 Season your meal: strategies and redundancies .............. 232
7 Path calculi ............................................... 233
8 Logics without the contraction rules ....................... 255
9 Conclusion ................................................. 260
Bibliography ............................................... 264
Index ...................................................... 270
Chapter 5 NORMAL FORM TRANSFORMATIONS ........................ 273
Matthias Baaz, Uwe Egly, and Alexander Leitsch
1 Introduction ............................................... 275
2 Notation and Definitions ................................... 278
3 On the Concept of Normal Form .............................. 287
4 Equivalence-Preserving Normal Forms ........................ 289
5 Skolem Normal Form ......................................... 295
6 Conjunctive Normal Form .................................... 306
7 Normal Forms in Nonclassical Logics ........................ 323
8 Conclusion ................................................. 328
Bibliography ............................................... 328
Index ...................................................... 332
Chapter 6 COMPUTING SMALL CLAUSE NORMAL FORMS ................ 335
Andreas Nonnengart and Christoph Weidenbach
1 Introduction ............................................... 337
2 Preliminaries .............................................. 338
3 Standard CNF-Translation ................................... 340
4 Formula Renaming ........................................... 347
5 Skolemization .............................................. 352
6 Simplification ............................................. 359
7 Bibliographic Notes ........................................ 363
8 Implementation Notes ....................................... 364
Bibliography ............................................... 365
Index ...................................................... 367
Part III Equality and other theories
Chapter 7 PARAMODULATION-BASED THEOREM PROVING ............... 371
Robert Nieuwenhuis and Albert Rubio
1 About this Chapter ......................................... 373
2 Preliminaries .............................................. 380
3 Paramodulation calculi ..................................... 385
4 Saturation procedures ...................................... 399
5 Paramodulation with constrained clauses .................... 414
6 Paramodulation with built-in equational theories ........... 421
7 Symbolic constraint solving ................................ 425
8 Extensions ................................................. 427
9 Perspectives ............................................... 429
Bibliography ............................................... 432
Index ...................................................... 440
Chapter 8 UNIFICATION THEORY ................................. 445
Franz Baader and Wayne Snyder
1 Introduction ............................................... 447
2 Syntactic unification ...................................... 450
3 Equational unification ..................................... 469
4 Syntactic methods for E-unification ........................ 488
5 Semantic approaches to E-unification ....................... 503
6 Combination of unification algorithms ...................... 513
7 Further topics ............................................. 519
Bibliography ............................................... 521
Index ...................................................... 531
Chapter 9 REWRITING .......................................... 535
Nachum Dershowitz and David A. Plaisted
1 Introduction ............................................... 537
2 Terminology ................................................ 541
3 Normal Forms and Validity .................................. 544
4 Termination Properties ..................................... 546
5 Church-Rosser Properties ................................... 559
6 Completion ................................................. 567
7 Relativized Rewriting ...................................... 574
8 Equational Theorem Proving ................................. 581
9 Conditional Rewriting ...................................... 585
10 Programming ................................................ 593
Bibliography ............................................... 597
Index ...................................................... 608
Chapter 10 EQUALITY REASONING IN SEQUENT-BASED CALCULI ........ 611
Anatoli Degtyarev and Andrei Voronkov
1 Introduction ............................................... 613
2 Translation of logic with equality into logic without
equality ................................................... 628
3 Free variable systems ...................................... 637
4 Early history .............................................. 644
5 Simultaneous rigid E-unification ........................... 646
6 Incomplete procedures for rigid E-unification .............. 653
7 Sequent-based calculi and paramodulation ................... 660
8 Equality elimination ....................................... 667
9 Equality reasoning in nonclassical logics .................. 679
10 Conclusion and open problems ............................... 691
Bibliography ............................................... 693
Calculi and inference rules ................................ 703
Index ...................................................... 704
Chapter 11 AUTOMATED REASONING IN GEOMETRY .................... 707
Shang-Ching Chou and Xiao-Shan Gao
1 A history review of automated reasoning in geometry ........ 709
2 Algebraic approaches to automated reasoning in geometry .... 712
3 Coordinate-free approaches to automated reasoning in
geometry ................................................... 732
4 AI approaches to automated reasoning in geometry ........... 734
5 Final remarks .............................................. 740
Bibliography ............................................... 741
Index ...................................................... 749
Chapter 12 SOLVING NUMERICAL CONSTRAINTS ..................... 751
Alexander Bockmayr and Volker Weispfenning
1 Introduction ............................................... 753
2 Linear constraints over fields ............................. 758
3 Linear diophantine constraints ............................. 779
4 Non-linear constraints over continuous domains ............. 802
5 Non-linear diophantine constraints ......................... 819
Bibliography ............................................... 823
Index ...................................................... 838
Part IV Induction
Chapter 13 THE AUTOMATION OF PROOF BY MATHEMATICAL
INDUCTION ..................................................... 845
Alan Bundy
1 Introduction ............................................... 847
2 Induction Rules ............................................ 848
3 Recursive Definitions and Datatypes ........................ 851
4 Inductive Proof Techniques ................................. 855
5 Theoretical Limitations of Inductive Inference ............. 863
6 Special Search Control Problems ............................ 865
7 Rippling ................................................... 876
8 The Productive Use of Failure .............................. 890
9 Existential Theorems ....................................... 894
10 Interactive Theorem Proving ................................ 898
11 Inductive Theorem Provers .................................. 900
12 Conclusion ................................................. 903
Bibliography ............................................... 904
Main Index ................................................. 909
Name Index ................................................. 911
Chapter 14 INDUCTIONLESS INDUCTION ............................ 913
Hubert Comon
1 Introduction ............................................... 915
2 Formal background .......................................... 919
3 General Setting of the Inductionless Induction Method ...... 925
4 Inductive completion methods ............................... 927
5 Examples of Axiomatizations  from the Literature .......... 938
6 Ground Reducibility ........................................ 948
7 A comparison between inductive proofs and proofs by
consistency ................................................ 957
Bibliography ............................................... 958
Index ...................................................... 961
Concept Index ................................................. 963
|
