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