Automated Theorem Proving

Proofs.- 6.5 Restrictions on the Form of Linear Proofs.- 6.6 The Lifting Lemma.- 6.7 Linear Proofs and Factoring.- Exercises for Chapter 6.- 7 HERBY: A Semantic-Tree Theorem Prover.- 7.1 Heuristics for Selecting Atoms.- 7.2 Additional Heuristics.- 7.2.1 List ordering heuristics.- 7.2.2 Preliminary phase (Phase 0): Base clause resolution heuristic (BCRH).- 7.2.3 Heuristic limiting the number of literals in a clause.- 7.2.4 Heuristic limiting the number of terms in a literal.- 7.2.5 Tree pruning heuristic.- 7.3 Assigning a Hash Code to a Literal and to a Clause.- 7.4 The Overall Algorithm.- 7.5 Obtaining a Resolution-Refutation Proof.- Exercises for Chapter 7.- 8 Using HERBY.- 8.1 Proving Theorems with HERBY: The Input File.- 8.2 HERBY's Convention on Naming the Output File.- 8.3 The Options Available to the User.- 8.3.1 Option to prove a set of theorems.- 8.3.2 Obtaining help by typing"?".- 8.4 User Interaction During the Construction.- 8.5 Option Examples.- 8.6 The Printout Produced by HERBY.- 8.7 A Second Example, the Printout Produced Using the r1 Option.- Exercises for Chapter 8.- 9 THEO: A Resolution-Refutation Theorem Prover.- 9.1 Iteratively Deepening Depth-First Search and Linear Proofs.- 9.2 Searching for a Linear-Merge Proof.- 9.3 Searching for a Linear-nc Proof.- 9.4 Searching for a Linear-Merge-nc Proof.- 9.5 The Extended Search Strategy.- 9.6 Bounding the Number of Literals in a Clause.- 9.7 Bounding the Number of Terms in a Literal.- 9.8 Bounding the Number of Different Variables in an Inference.- 9.9 Ordering Clauses at Each Node.- 9.10 A Hash Table that Stores Information About Clauses.- 9.10.1 Assigning a hash code to a literal.- 9.10.2 Assigning a hash code to a clause.- 9.10.3 Entering clauses in clause_hash_table.- 9.11 Using Entries in clause_hash_table.- 9.12 Unit Clauses.- 9.12.1 Obtaining a contradiction.- 9.12.2 Unit hash table resolutions.- 9.13 Assigning Hash Codes to Instances and Variants of Unit Clauses.- 9.14 Other Hash Codes Generated.- 9.15 The Use of S-Subsumption to Restrict the Search Space.- 9.16 Extending the Search on Merge Clauses.- 9.17 Extending the Search on Clauses from the Negated Conclusion.- 9.18 Do Not Factor Within the Search Horizon.- 9.19 Clauses in the Extended Search Region Must Havea Constant.- 9.20 In the Extended Search Region, Do Not Search the Single Inference of a Long Clause.- 9.21 Eliminate Tautologies.- 9.22 Special Consideration of the Predicate Equal.- 9.23 Assembling the Proof.- 9.24 eliminate: Simplifying the Base Clauses.- 9.25 Summary of THEO's Search Strategy.- Exercises for Chapter 9.- 10 Using THEO.- 10.1 Proving Theorems with THEO: The Input File.- 10.2 THEO's Convention on Naming the Output File.- 10.3 The Options Available to the User.- 10.3.1 Options that determine the search strategy.- 10.3.2 Options that determine the information observed by the user.- 10.3.3 Option to prove a set of theorems.- 10.3.4 Obtaining help by typing"?".- 10.4 User Interaction During the Search.- 10.5 Option Examples.- 10.6 The Printout Produced by THEO.- 10.7 A Second Example: The Printout Produced with the d1 Option.- Exercises for Chapter 10.- 11 A Look at the Source Code of HERBY.- 11.1 Source Files for HERBY.- 11.2 Function Linkage in HERBY.- 11.3 A Brief Description of the Main Functions in HERBY.- 11.4 Machine Code Representation of a Clause in HERBY.- 11.4.1 The clause header.- 11.4.2 The literal header.- 11.4.3 Representing the terms of a literal.- 11.4.4 An example of the representation.- 11.5 Major Arrays in HERBY.- Exercises for Chapter 11.- 12 A Look at the Source Code of THEO.- 12.1 Source Files for THEO.- 12.2 Function Linkage in THEO.- 12.3 A Brief Description of the Main Functions in THEO.- 12.4 Machine Code Representation of a Clause in THEO.- 12.5 Major Arrays in THEO.- 12.6 Functions Related to clause_hash_table.- 12.7 Functions Related to cl_array.- Exercises for Chapter 12.- 13 The CADE ATP System Competitions and Other Theorem Provers.- 13.1 Gandalf.- 13.2 Otter.- Exercises for Chapter 13.- Appendix A Answers to Selected Exercises.- Appendix B List of Wffs and Theorems in the Directories WFFS, THEOREMS, GEOMETRY, and THMSMISC.