# Automated Theorem Proving: Theory and Practice, Volume 1

Springer Science & Business Media, Dec 15, 2000 - Mathematics - 231 pages
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