file-size file-name
file-description
Please see my web page and that of the ATP group at UT.
JAR 11: pages 293-314, 1993.
SET-VAR atp.106 W.W. Bledsoe and Guohui Feng Dec 1991 Computer Science Department The University of Texas at Austin Austin, Texas 78703ABSTRACT: In this paper, we describe the rules of the SET-VAR prover, which is an extension of Resolution, and which handles theorems in a subset of second order logic. We also give example proofs using the system, and show that the rules are sound. And we conjecture that the prover is complete for a certain extension of first order logic which includes many of the theorems of real analysis. This System is based on an earlier "set variable" prover, implemented in natural deduction.
A Precondition Prover for Analogy
W.W. Bledsoe Computer Science Department The University of Texas at Austin Austin, Texas 78712We describe here a prover PC that normally acts as an ordinary theorem prover, but which returns a ``precondition'' when it is unable to prove the given formula. If F is the formula attempted to be proved and PC returns the precondition Q, then (Q --> F) is a theorem (that PC can prove). This prover, PC, uses a Proof-Plan. In its simplest mode, when there is no proof-plan, it acts like ordinary Abduction. We show here how this method can be used to derive certain proofs by analogy. To do this, it uses a proof-plan from a given guiding proof to help construct the proof of a similar theorem, by ``debugging'' (automatically) that proof-plan.
We show here the analogy proofs of a few simple example theorems and one hard pair, Ex4 and Ex4L. The given proof-plan for Ex4 is used by the system to prove automatically Ex4; and that same proof-plan is then used to prove Ex4L, during which the proof-plan is ``debugged'' (automatically). These two examples are similar to two other, more difficult, theorems from the Theory of Resolution, namely GCR (the ground completeness of Resolution) and GCLR (the ground completeness of Lock Resolution). GCR and and GCLR have also been handled, in essence, by this system but not completed in all their details.
ATP 119 May 1993 SET-VAR Implementation W. W. Bledsoe Computer Science Department University of Texas Austin, Texas 78712This paper describes an implementation of the SET-VAR proof procedure [1]. Te program itself, found in the file, SET-VAR.LISP, is written in LISP and attempts to prove theorems in FOL-S a certain extension of First-order logic (see below). A call to (SET-VAR THM) causes it to attempt to automatically prove the theorem, THM. Even though we believe that SET-VAR is complete for FOL-S, we know that this implementation is not, because we have made several restrictions (see below) in order to speed up the search. But we believe that it still retains most of the generality of SET-VAR itself.
Using SET-VAR to Prove the Heine Borel Theorem W. W. Bledsoe ATP 120 25 January 1994
Heine-Borel Theorem Analogy Example ATP.124 W. W. Bledsoe August 1994ABSTRACT.
We give here a pair of theorems that we hope to use in our Analogy Theorem Proving experiments. They both are Heine-Borel Theorems, the first for the Real Line, R1, and the second for two dimensional real space, R2. The basic idea is to use a proof of the first as a guide to produce (automatically) a proof of the second. We have not yet produced such an automatic proof; we give these examples and the information below, only as material for proceeding with the analogy process.
CONTENTS
The Creation and Use of a Knowledge Base of Mathematical Theorems and Definitions Benjamin Shults Department of Mathematics University of Texas at Austin Austin, TX 78712 bshults@math.utexas.eduIPR is an automatic theorem-proving system intended particularly for use in higher-level mathematics. It discovers the proofs of theorems in mathematics applying known theorems and definitions. Theorems and definitions are stored in the knowledge base in the form of sequents rather than formulas or rewrite rules. Because there is more easily-accessible information in a sequent than there is in the formula it represents, a simple algorithm can be used to search the knowledge base for the most useful theorem or definition to be used in the theorem-proving process. This paper describes how the sequents in the knowledge base are formed from theorems stated by the user and how the knowledge base is used in the theorem-proving process. An example of a theorem proved and the English proof output are also given.
A Framework for the Creation and Use of a Knowledge Base of Mathematical Theorems and Definitions Benjamin Shults Department of Mathematics University of Texas at Austin Austin, TX 78712 bshults@math.utexas.eduThis paper covers the framework underlying the IPR prover, some of whose success is illustrated in ATP-127. The presentation here is more clear than the presentation in ATP-127 but this does not include the examples of theorems proved.
Abstract:
A mathematician knows thousands of theorems and definitions and is able to choose just the needed results and use them at just the right time in the theorem-proving process. The problem of codifying some bit of this process is the topic of this paper.
IPR is an automatic theorem-proving system intended particularly for use in mathematics. It discovers the proofs of theorems in mathematics by applying known theorems and definitions from a knowledge base. Theorems and definitions are stored in the knowledge base in the form of ``sequents'' rather than formulas or rewrite rules. The sequents---into which a theorem is reduced before being put into the knowledge base---consistently mirror the ways a human might use the theorem. Because the data are in this form, natural fetching algorithms can be used to search the knowledge base for the most useful theorem to be used in the theorem-proving process.
JAR 6: 341-359, 1990
ATP 89j 24 May 1990 CHALLENGE PROBLEMS IN ELEMENTARY CALCULUS W. W. Bledsoe The University of TexasThe following is a list of challenge problems for automated provers. They are based on the theorem in calculus that the sum of two continuous functions is continuous (called Lim+).