📄 http:^^www.ma.utexas.edu^users^bshults^ipr^atp.html
字号:
Date: Tue, 07 Jan 1997 15:42:11 GMTServer: NCSA/1.4.2Content-type: text/html<title>Benji's ATP research page</title><body bgcolor="#ffffff" text="#000000" link="#0000ee" vlink="551a8b" alink="ff0000"><h1>ATP research</h1><h2>The IPR System</h2>The IPR system proves theorems in mathematics by <!WA0><!WA0><!WA0><ahref="http://www.ma.utexas.edu/users/bshults/IPR/knowledge-using.html">usinga knowledge base</a> of theorems, axioms and definitions. Rather thanapplying all of its knowledge systematically, the IPR prover picks asingle bit of information at a time according to its determination ofthe current usefulness of the information.<p><b>The IPR Framework</b><p>IPR uses the tableaux-calculus for first-order logic theorem proving.This method has some properties which recommend its use by proverswhich are intended to communicate with non-expert humans. A branchof a tableau can be displayed as a sequent.<p>The knowledge is stored in the knowledge base in the form of sequents.When the theorem prover reaches the q-limit, it chooses a branch ofthe tableau which needs more work and searches the knowledge base forthe most useful bit of information. It determines which theorem touse by comparing the branch (as a sequent) to the theorems in theknowledge base.<p>The success of the prover on traditionally difficult problems showsthat this method of storing and fetching theorems has merit.<p>Two tech reports offer more information about the IPR framework. [<!WA1><!WA1><!WA1><Ahref="http://www.ma.utexas.edu/users/bshults/IPR/TR-FLAIRS97.ps">Intelligentuse of a knowledge base in automated theorem proving.</a>,<!WA2><!WA2><!WA2><ahref="http://www.ma.utexas.edu/users/bshults/IPR/TR-AAR.ps">Challengeproblems in first-order theories.</a>] I am currently preparing morepapers for submission. I will attach some of these reports to thispage as soon as possible.<p><b>The English Interface</b><p>All of the output from IPR is in English. When it finds a proof, itoutputs a description of the steps it took and the theorems it appliedin a form which might appear in a textbook.If the user chooses to interact during the theorem-proving process,IPR displays each branch of the proof in English. For example:<p><dl><dd>Suppose all of the following:<dd>1. (_B) is a linearly independent subset of the vector space (_V)<dd>2. (_B0) is a basis of the vector space (_V)<dd>and show that<dd>the union of E and F is a basis of the vector space (_V)</dl>Here, (_B), (_B0) and (_V) represent constants and E and F arevariables.<p><b><!WA3><!WA3><!WA3><ahref="http://www.ma.utexas.edu/users/bshults/IPR/examples.html">Examplesof Proofs</a></b><p>The first hard theorem IPR proved in 1994 was the 101st labeledtheorem from John Kelley's <i>General Topology</i>:<p><em>If a product is locally compact, then each coordinate space islocally compact.</em><p>IPR proved this in the presence of 100 theorems. Each of the theoremswere taken from earlier sections of the text related to the predicatesinvolved in the theorem. IPR analyses the knowledge base once foreach formula in the proof. When it needs to apply a theorem, itcompares the usefulness of the theorems to the current situation andchoses the single theorem which if considers most useful. In thisproof, IPR did not use any of the theorems except the three which areneeded in the proof. It chose those theorems and found the shortestpossible proof without wasting any time on the other knowledge.<p>A second example, this one involving much more complex reasoning, isthe following:<p><em>If S is a Hausdorff topological space, then the diagonal of SXS isclosed.</em><p>The proof of this theorem (given a certain knowledge base) requiresthe application of twelve theorems. The proof also requires someequality reasoning and a fairly tricky variable instantiation. Thisvariable instantiation is needed because the proof involves finding anopen set in SXS containing an arbitrary point in SXS and disjoint fromthe diagonal.<p> In the presence of a knowledge base containing over12 theorems, IPR finds this proof in under a minute on my PC at home.<p>Since my dissertation will be on this topic, expect this part of theweb to grow.<p>This work was done aspart of the <!WA4><!WA4><!WA4><ahref="http://www.ma.utexas.edu/users/bshults/ATP/home.html">AutomatedTheorem Proving Group</a> at <!WA5><!WA5><!WA5><aHREF="http://wwwhost.cc.utexas.edu">The University of Texas atAustin.</a><P><hr><!WA6><!WA6><!WA6><a href="http://www.ma.utexas.edu/users/bshults">Benjamin Shults</a>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -