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 78703
ABSTRACT: 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 78712
This 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 1994
ABSTRACT. 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 Texas
The 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+).