📄 ftp:^^ftp.cs.utexas.edu^pub^bshults^atp-tech-reports^index.html
字号:
<html><title>Index</title><h1>Index of /pub/bshults/ATP-tech-reports</h1>This page describes the contents of this directory in the format:<p> file-size file-name<p> file-description<p>Please see <a href="http://www.ma.utexas.edu/users/bshults">my</a> webpage and that of <ahref="http://www.ma.utexas.edu/users/bshults/ATP">the ATP group</a> atUT.<p><hr> 47277 <ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-106.ascii">atp-106.ascii</a><p>JAR 11: pages 293-314, 1993.<p><pre> SET-VAR atp.106 W.W. Bledsoe and Guohui Feng Dec 1991 Computer Science Department The University of Texas at Austin Austin, Texas 78703</pre> ABSTRACT: In this paper, we describe the rules of the SET-VAR prover, whichis an extension of Resolution, and which handles theorems in a subset of second order logic. We also give example proofs using the system, andshow that the rules are sound. And we conjecture that the prover is completefor a certain extension of first order logic which includes many of thetheorems of real analysis. This System is based on an earlier "set variable"prover, implemented in natural deduction.<p><hr><dt> 406636 <ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-116.ps">atp-116.ps</a><dt> 89738 <ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-116.tex">atp-116.tex</a><p> A Precondition Prover for Analogy<p> <pre>W.W. Bledsoe Computer Science Department The University of Texas at Austin Austin, Texas 78712</pre>We describe here a prover PC that normally acts as an ordinary theoremprover, but which returns a ``precondition'' when it is unable toprove the given formula. If <em>F</em> is the formula attempted to beproved and PC returns the precondition <em>Q</em>, then <em>(Q -->F)</em> is a theorem (that PC can prove). This prover, PC, uses a<em>Proof-Plan</em>. In its simplest mode, when there is noproof-plan, it acts like ordinary <em>Abduction</em>. We show here howthis method can be used to derive certain proofs by <em>analogy</em>.To do this, it uses a proof-plan from a given <em>guiding</em> proofto help construct the proof of a similar theorem, by ``debugging''(automatically) that proof-plan.<p>We show here the analogy proofs of a few simple example theorems andone hard pair, Ex4 and Ex4L. The given proof-plan for Ex4 is used bythe system to prove automatically Ex4; and that same proof-plan isthen used to prove Ex4L, during which the proof-plan is ``debugged''(automatically). These two examples are similar to two other, moredifficult, theorems from the <em>Theory of Resolution</em>, namely GCR(the ground completeness of Resolution) and GCLR (the groundcompleteness of Lock Resolution). GCR and and GCLR have also beenhandled, in essence, by this system but not completed in all theirdetails.<p><hr> 22460 <ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-119.ascii">atp-119.ascii</a><p><pre> ATP 119 May 1993 SET-VAR Implementation W. W. Bledsoe Computer Science Department University of Texas Austin, Texas 78712</pre>This paper describes an implementation of the SET-VAR proofprocedure [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.<p><hr> 36777 <ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-120.ascii">atp-120.ascii</a><p><pre> Using SET-VAR to Prove the Heine Borel Theorem W. W. Bledsoe ATP 120 25 January 1994</pre><dl><dt>Theorem (Heine-Borel). If G is a family of open sets on the real line<dd> which cover the closed interval [a,b], then some finite subset<dd> H of G also covers [a,b].<p></dl><hr> 43846 <ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-124.ascii">atp-124.ascii</a><p><pre> Heine-Borel Theorem Analogy Example ATP.124 W. W. Bledsoe August 1994</pre>ABSTRACT. <p>We give here a pair of theorems that we hope to use in our AnalogyTheorem Proving experiments. They both are Heine-Borel Theorems,the first for the Real Line, R1, and the second for two dimensionalreal space, R2. The basic idea is to use a proof of the first asa guide to produce (automatically) a proof of the second. We have not yet produced such an automatic proof; we give these examplesand the information below, only as material for proceeding withthe analogy process. <p> CONTENTS<p><ul><li> 0. Introduction.<li> 1. Heine-Borel-1<li> 2. Heine-Borel-2<li> 3. Converting the Proof Plan<li> 4. Remarks<li> Appendix A. Informal Proof of the Heine-Borel Theorem<li> Appendix B. LISP version of the Plans given in Sections 1 and 2.<li> Appendix C. LISP version of an earlier version of Plans for HB1 and HB2.<li> Appendix D. Examples of difficult FOL theorems (but easy for humans).<li> Appendix E. A LINEAR plan for HB1.</ul><hr> 298173 <ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-127.ps">atp-127.ps</a><p><pre>The Creation and Use of a Knowledge Base of Mathematical Theorems and DefinitionsBenjamin Shults Department of Mathematics University of Texas at Austin Austin, TX 78712 bshults@math.utexas.edu</pre>IPR is an automatic theorem-proving system intended particularly foruse in higher-level mathematics. It discovers the proofs of theoremsin mathematics applying known theorems and definitions. Theorems anddefinitions are stored in the knowledge base in the form of sequentsrather than formulas or rewrite rules. Because there is moreeasily-accessible information in a sequent than there is in theformula it represents, a simple algorithm can be used to search theknowledge base for the most useful theorem or definition to be used inthe theorem-proving process. This paper describes how the sequents inthe knowledge base are formed from theorems stated by the user and howthe knowledge base is used in the theorem-proving process. An exampleof a theorem proved and the English proof output are also given.<p><hr> 273543 <ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-127a.ps">atp-127a.ps</a><p><pre>A Framework for the Creation and Use of a Knowledge Base of Mathematical Theorems and DefinitionsBenjamin Shults Department of Mathematics University of Texas at Austin Austin, TX 78712 bshults@math.utexas.edu</pre>This paper covers the framework underlying the IPR prover, some ofwhose success is illustrated in ATP-127. The presentation here ismore clear than the presentation in ATP-127 but this does not includethe examples of theorems proved.<p>Abstract:<p>A mathematician knows thousands of theorems and definitions and isable to choose just the needed results and use them at just the righttime in the theorem-proving process. The problem of codifying somebit of this process is the topic of this paper.<p>IPR is an automatic theorem-proving system intended particularly foruse in mathematics. It discovers the proofs of theorems inmathematics by applying known theorems and definitions from aknowledge base. Theorems and definitions are stored in the knowledgebase in the form of ``sequents'' rather than formulas or rewriterules. The sequents---into which a theorem is reduced before beingput into the knowledge base---consistently mirror the ways a humanmight use the theorem. Because the data are in this form, naturalfetching algorithms can be used to search the knowledge base for themost useful theorem to be used in the theorem-proving process.<p><hr> 60458 <ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-89j.ascii">atp-89j.ascii</a><p>JAR 6: 341-359, 1990<p><pre> ATP 89j 24 May 1990 CHALLENGE PROBLEMS IN ELEMENTARY CALCULUS W. W. Bledsoe The University of Texas</pre>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+).<p><hr><em>This page is maintained by <ahref="http://www.ma.utexas.edu/users/bshults">Benjamin Shults</a>.Please email me at </em>bshults@math.utexas.edu <em>if you havesuggestions or further information.</em><p>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -