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
1152
Part V Higher-order logic and logical frameworks
Classical Type Theory
965
44
Peter B. Andrews
Introduction to type theory
967
10
Metatheoretical foundations
977
10
Proof search
987
11
Conclusion
998
11
Bibliography
999
6
Index
1005
4
Higher-Order Unification and Matching
1009
54
Gilles Dowek
Type Theory and Other Set Theories
1011
7
Simply Typed λ-calculus
1018
6
Undecidability
1024
4
Huet's Algorithm
1028
7
Scopes Management
1035
6
Decidable Subcases
1041
8
Unification in λ-calculus with Dependent Types
1049
14
Bibliography
1054
7
Index
1061
2
Logical Frameworks
1063
86
Frank Pfenning
Introduction
1065
2
Abstract syntax
1067
8
Judgments and deductions
1075
20
Meta-programming and proof search
1095
13
Representing meta-theory
1108
11
Appendix: the simply-typed λ-calculus
1119
4
Appendix: the dependently typed λ-calculus
1123
7
Conclusion
1130
19
Bibliography
1135
10
Index
1145
4
Proof-Assistants Using Dependent Type Systems
1149
92
Henk Barendregt
Herman Geuvers
Proof checking
1151
2
Type-theoretic notions for proof checking
1153
27
Type systems for proof checking
1180
31
Proof-development in type systems
1211
12
Proof assistants
1223
18
Bibliography
1230
5
Index
1235
3
Name index
1238
3
Part VI Nonclassical logics
Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations
1241
114
Jurgen Dix
Ulrich Furbach
Ilkka Niemela
General Nonmonotonic Logics
1244
16
Automating General Nonmonotonic Logics
1260
20
From Automated Reasoning to Disjunctive Logic Programming
1280
17
Nonmonotonic Semantics of Logic Programs
1297
14
Implementing Nonmonotonic Semantics
1311
21
Benchmarks
1332
8
Conclusion
1340
15
Bibliography
1341
11
Index
1352
3
Automated Deduction For Many-Valued Logics
1355
48
Matthias Baaz
Christian G. Fermiller
Gernot Salzer
Introduction
1357
1
What is a many-valued logic?
1358
3
Classification of proof systems for many-valued logics
1361
7
Signed logic: reasoning classically about finitely-valued logics
1368
9
Signed resolution
1377
12
An example
1389
4
Optimization of transformation rules
1393
2
Remarks on infinitely-valued logics
1395
8
Bibliography
1396
5
Index
1401
2
Encoding Two-Valued Nonclassical Logics in Classical Logic
1403
84
Hans Jurgen Ohlbach
Andreas Nonnengart
Maarten de Rijke
Dov M. Gabbay
Introduction
1405
5
Background
1410
9
Encoding consequence relations
1419
4
The standard relational translation
1423
17
The functional translation
1440
15
The semi-functional translation
1455
10
Variations and alternatives
1465
10
Conclusion
1475
12
Bibliography
1477
7
Index
1484
3
Connections in Nonclassical Logics
1487
94
Arild Waaler
Introduction
1489
2
Prelude: Connections in classical first-order logic
1491
25
Labelled systems
1516
12
Propositional intuitionistic logic
1528
17
First-order intuitionistic logic
1545
8
Normal modal logics up to S4
1553
14
The S5 family
1567
14
Bibliography
1573
4
Index
1577
4
Part VII Decidable classes and model building
Reasoning in Expressive Description Logics
1581
54
Diego Calvanese
Giuseppe De Giacomo
Maurizio Lenzerini
Daniele Nardi
Introduction
1583
3
Description Logics
1586
7
Description Logics and Propositional Dynamic Logics
1593
5
Unrestricted Model Reasoning
1598
12
Finite Model Reasoning
1610
9
Beyond Basic Description Logics
1619
7
Conclusions
1626
9
Bibliography
1626
7
Index
1633
2
Model Checking
1635
156
Edmund M. Clarke
Bernd-Holger Schlingloff
Introduction
1637
4
Logical Languages, Expressiveness
1641
13
Second Order Languages
1654
16
Model Transformations and Properties
1670
11
Equivalence reductions
1681
8
Completeness
1689
11
Decision Procedures
1700
11
Basic Model Checking Algorithms
1711
13
Modelling of Reactive Systems
1724
11
Symbolic Model Checking
1735
16
Partial Order Techniques
1751
4
Bounded Model Checking
1755
4
Abstractions
1759
5
Compositionality and Modular Verification
1764
3
Further Topics
1767
24
Bibliography
1774
14
Index
1788
3
Resolution Decision Procedures
1791
62
Christian G. Fermuller
Alexander Leitsch
Ullrich Hustadt
Tanel Tammet
Introduction
1793
1
Notation and definitions
1794
8
Decision procedures based on ordering refinements
1802
12
Hyperresolution as decision procedure
1814
16
Resolution decision procedures for description logics
1830
12
Related work
1842
11
Bibliography
1843
4
Index
1847
6
Part VIII Implementation
Term Indexing
1853
112
R. Sekar
I. V. Ramakrishnan
Andrei Voronkov
Introduction
1855
4
Background
1859
7
Data structures for representing terms and indexes
1866
4
A common framework for indexing
1870
5
Path indexing
1875
8
Discrimination trees
1883
8
Adaptive automata
1891
9
Automata-driven indexing
1900
8
Code trees
1908
9
Substitution trees
1917
5
Context trees
1922
2
Unification factoring
1924
3
Multiterm indexing
1927
7
Issues in perfect filtering
1934
5
Indexing modulo AC-theories
1939
4
Elements of term indexing
1943
8
Indexing in practice
1951
4
Conclusion
1955
10
Bibliography
1957
5
Index
1962
3
Combining Superposition, Sorts and Splitting
1965
50
Christoph Weidenbach
What This Chapter is (not) About
1967
2
Foundations
1969
4
A First Simple Prover
1973
8
Inference and Reduction Rules
1981
19
Global Design Decisions
2000
15
Bibliography
2008
3
Links to Saturation Based Provers
2011
1
Index
2012
3
Model Elimination and Connection Tableau Procedures
2015
100
Reinhold Letz
Gernot Stenz
Introduction
2017
1
Clausal Tableaux and Connectedness
2018
18
Further Structural Refinements of Clausal Tableaux
2036
4
Global Pruning Methods in Model Elimination
2040
9
Shortening of Proofs
2049
13
Completeness of Connection Tableaux
2062
8
Architectures of Model Elimination Implementations
2070
22
Implementation of Refinements by Constraints
2092
10
Experimental Results
2102
5
Outlook
2107
8
Bibliography
2109
4
Index
2113
2
Concept Index
2115