## Automated Theorem Proving: Theory and Practice, Volume 1As 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 |

207 | |

Answers to Selected Exercises | 211 |

List of Wffs and Theorems in the Directories WFFS THEOREMS GEOMETRY and THMSMISC | 219 |

225 | |

### Common terms and phrases

A.THM Algorithm assigned automated theorem proving axioms base clauses binary factoring binary resolvent C1 and C2 clause on clist clause_hash_table clauses C1 closed semantic tree COMPILE constant construct a closed dependent depth depth-first search described in Section eliminate equal(A,B Equal(x,y Euclidean geometry example Exercises for Chapter failure node find a proof first-order predicate calculus function Gandalf hash code hash table resolution Herbrand base Herbrand universe inferences interpretation iteratively deepening linear proof linear-merge proof linear-nc proof makefile maximum number merge clause MFABB negated conclusion NULL clause number of literals number of terms options Phase predicate calculus Proof Found prove theorems qxxd resolution-refutation proof s-subsumed search horizon search tree second iteration set of clauses shown in Figure Skolem function source code Step subsumes subsumption tells THEO TPTP Problem Library transformation unit clause unit hash table unitjist variables Well-Formed Formulas wffs yield the NULL