Index of /pub/bshults/ATP-tech-reports

This page describes the contents of this directory in the format:

file-size file-name

file-description

Please see my web page and that of the ATP group at UT.


47277 atp-106.ascii

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.


406636 atp-116.ps
89738 atp-116.tex

A Precondition Prover for Analogy

W.W. Bledsoe 
Computer Science Department 
The University of Texas at Austin 
Austin, Texas 78712
We 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.


22460 atp-119.ascii

                                                           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.


36777 atp-120.ascii

     Using SET-VAR to Prove the Heine Borel Theorem
                W. W. Bledsoe                             ATP 120
                                                  25 January 1994
Theorem (Heine-Borel). If G is a family of open sets on the real line
which cover the closed interval [a,b], then some finite subset
H of G also covers [a,b].


43846 atp-124.ascii

         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


298173 atp-127.ps

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


273543 atp-127a.ps

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


60458 atp-89j.ascii

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


This page is maintained by Benjamin Shults. Please email me at bshults@math.utexas.edu if you have suggestions or further information.