Automated Theorem Proving: Theory and Practice

'1 A Brief Introduction to COMPILE, HERBY, and THEO.- 1.1 COMPILE.- 1.1.1 Creating an executable version of COMPILE.- 1.1.2 Running COMPILE.- 1.2 HERBY.- 1.2.1 Creating an executable version of HERBY.- 1.2.2 Running HERBY.- 1.3 THEO.- 1.3.1 Creating an executable version of THEO.- 1.3.2 Running THEO.- 1.4 The Accompanying Software.- Exercises for Chapter 1.- 2 Predicate Calculus, Well-Formed Formulas and Theorems.- 2.1 The Syntax of Well-Formed Formulas.- 2.2 Examples of Well-Formed Formulas.- 2.3 Creating Well-Formed Formulas from Statements in English.- 2.4 Interpretations of Well-Formed Formulas.- 2.5 A Set of Axioms to Prove Theorems in Group Theory.- 2.6 An Axiom System for Euclidean Geometry.- Exercises for Chapter 2.- 3 COMPILE: Transforming Well-Formed Formulas to Clauses.- 3.1 The Transformation Procedure of COMPILE.- 3.2 Using COMPILE.- 3.3 Examples of the Transformation of Wffs to Clauses.- Exercises for Chapter 3.- 4 Inference Procedures.- 4.1 An Informal Introduction to Binary Resolution and Binary Factoring.- 4.2 The Processes of Substitution and Unification.- 4.3 Subsumption.- 4.4 The Most General Unifier.- 4.5 Determining All Binary Resolvents of Two Clauses.- 4.6 Merge Clauses.- 4.7 Determining All Binary Factors of a Clause.- 4.8 A Special Case of Binary Resolution: Modus Ponens.- 4.9 Clauses and Subsumption.- 4.10 Logical Soundness.- 4.11 Base Clauses and Inferred Clauses.- Exercises for Chapter 4.- 5 Proving Theorems by Contracting Closed Semantic Trees.- 5.1 The Herbrand Universe of a Set of Clauses.- 5.2 The Herbrand Base of a Set of Clauses.- 5.3 An Interpretation on the Herbrand Base.- 5.4 Establishing the Unsatisfiability of a Set of Clauses.- 5.5 Semantic Trees.- 5.6 Noncanonical Semantic Trees.- Exercises for Chapter 5.- 6 Resolution-Refutation Proofs.- 6.1 Examples of Resolution-Refutation Proofs.- 6.2 The Depth and Length of Resolution-Refutation Proofs.- 6.3 Obtaining a Resolution-Refutation Proof from a Semantic Tree.- 6.4 Linear 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 Ass