Automated Theorem Proving: Theory and Practice

ISBN-13: 9780387950754 / Angielski / Twarda / 2000 / 231 str.

Monty Newborn; Monroe Newborn

Opis

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

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.