Automated Theorem Proving: Theory and Practice, Volume 1

Front Cover
Springer Science & Business Media, Jan 1, 2001 - Computers - 231 pages
0 Reviews
As the 21st century begins, the power of our magical new tool and partner, the computer, is increasing at an astonishing rate. Computers that perform billions of operations per second are now commonplace. Multiprocessors with thousands of little computers - relatively little! -can now carry out parallel computations and solve problems in seconds that only a few years ago took days or months. Chess-playing programs are on an even footing with the world's best players. IBM's Deep Blue defeated world champion Garry Kasparov in a match several years ago. Increasingly computers are expected to be more intelligent, to reason, to be able to draw conclusions from given facts, or abstractly, to prove theorems-the subject of this book. Specifically, this book is about two theorem-proving programs, THEO and HERBY. The first four chapters contain introductory material about automated theorem proving and the two programs. This includes material on the language used to express theorems, predicate calculus, and the rules of inference. This also includes a description of a third program included with this package, called COMPILE. As described in Chapter 3, COMPILE transforms predicate calculus expressions into clause form as required by HERBY and THEO. Chapter 5 presents the theoretical foundations of seman tic tree theorem proving as performed by HERBY. Chapter 6 presents the theoretical foundations of resolution-refutation theorem proving as per formed by THEO. Chapters 7 and 8 describe HERBY and how to use it.
  

What people are saying - Write a review

We haven't found any reviews in the usual places.

Contents

A Brief Introduction to COMPILE HERBY and THEO
1
11 COMPILE
2
12 HERBY
3
13 THEO
4
14 The Accompanying Software
5
Exercises for Chapter 1
6
Predicate Calculus WellFormed Formulas and Theorems
7
22 Examples of WellFormed Formulas
9
91 Iteratively Deepening DepthFirst Search and Linear Proofs
114
92 Searching for a LinearMerge Proof
116
93 Searching for a Linearnc Proof
118
94 Searching for a LinearMergenc Proof
119
95 The Extended Search Strategy
120
96 Bounding the Number of Literals in a Clause
121
99 Ordering Clauses at Each Node
122
9102 Assigning a hash code to a clause
124

25 A Set of Axioms to Prove Theorems in Group Theory
12
26 An Axiom System for Euclidean Geometry
14
Exercises for Chapter 2
17
COMPILE Transforming WellFormed Formulas to Clauses
21
32 Using COMPILE
24
33 Examples of the Transformation of Wffs to Clauses
25
Inference Procedures
29
42 The Processes of Substitution and Unification
31
43 Subsumption
32
44 The Most General Unifier
33
46 Merge Clauses
37
Modus Ponens
38
49 Clauses and Subsumption
39
410 Logical Soundness
40
Proving Theorems by Constructing Closed Semantic Trees
43
52 The Herbrand Base of a Set of Clauses
44
53 An Interpretation on the Herbrand Base
45
55 Semantic Trees
47
56 Noncanonical Semantic Trees
50
Exercises for Chapter 5
52
ResolutionRefutation Proofs
53
61 Examples of ResolutionRefutation Proofs
54
62 The Depth and Length of ResolutionRefutation Proofs
58
64 Linear Proofs
64
65 Restrictions on the Form of Linear Proofs
71
66 The Lifting Lemma
79
67 Linear Proofs and Factoring
80
Exercises for Chapter 6
82
HERBY A SemanticTree Theorem Prover
85
72 Additional Heuristics
91
Base clause resolution heuristic BCRH
93
725 Treepruning heuristic
94
75 Obtaining a ResolutionRefutation Proof
95
Using HERBY
97
82 HERBYs Convention on Naming the Output File
98
831 Option to prove a set of theorems
99
832 Obtaining help by typing ?
100
The Printout Produced Using the r1 Option
107
Exercises for Chapter 8
111
THEO A ResolutionRefutation Theorem Prover
113
911 Using Entries in clause hash table
125
9122 Unit Hash Table Resolutions
128
913 Assigning Hash Codes to Instances and Variants of Unit Clauses
130
914 Other Hash Codes Generated
131
915 The Use of SSubsumption to Restrict the Search Space
132
918 Do Not Factor Within the Search Horizon
133
Simplifying the Base Clauses
134
925 Summary of THEOs Strategy
135
Exercises for Chapter 9
137
Using THEO
139
102 THEOs Convention on Naming the Output File
140
1031 Options that determine the search strategy
141
1032 Options that determine the information observed by the user
142
1033 Option to prove a set of theorems
143
104 User Interaction During the Search
144
106 The Printout Produced by THEO
145
The Printout Produced with the d1 Option
149
Exercises for Chapter 10
155
A Look at the Source Code of HERBY
161
112 Function Linkage in HERBY
164
114 Machine Code Representation of a Clause in HERBY and THEO
165
1142 The literal header
167
1144 An example of the representation
168
115 Major Arrays in HERBY
170
Exercises for Chapter 11
172
A Look at the Source Code of THEO
173
122 Function Linkage in THEO
174
124 Machine Code Representation of a Clause in THEO
178
126 Functions Related to clause_hash_table
179
127 Functions Related to cl_array
180
The CADE ATP System Competitions and Other Theorem Provers
181
131 Gandalf
182
132 Otter
190
Exercises for Chapter 13
204
Bibliography
207
Answers to Selected Exercises
211
List of Wffs and Theorems in the Directories WFFS THEOREMS GEOMETRY and THMSMISC
219
Index
225
Copyright

Common terms and phrases

References to this book

All Book Search results »

Bibliographic information