Automated Theorem Proving: Theory and Practice

ISBN-13: 9781461265191 / Angielski / Miękka / 2013 / 231 str.

Monty Newborn

Opis

This text and software package introduces readers to automated theorem proving, while providing two approaches implemented as easy-to-use programs. These are semantic-tree theorem proving and resolution-refutation theorem proving. The early chapters introduce first-order predicate calculus, well-formed formulae, and their transformation to clauses. Then the author goes on to show how the two methods work and provides numerous examples for readers to try their hand at theorem-proving experiments. Each chapter comes with exercises designed to familiarise the readers with the ideas and with the software, and answers to many of the problems.

Spis treści

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 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.