📄 http:^^www.ma.utexas.edu^users^bshults^ipr^knowledge-using.html
字号:
Date: Tue, 07 Jan 1997 15:42:07 GMTServer: NCSA/1.4.2Content-type: text/html<html><title>Using Knowledge Automatically</title><body bgcolor="#ffffff" text="#000000" link="#0000ee" vlink="551a8b" alink="ff0000"><h1>Using Knowledge Automatically</h1>The <em> Bledsoe Philosophy </em> of automated theorem proving isbasically the belief that automated provers must use human-likemethods in order to be successful in mathematics. <p>When a mathematician tries to prove a theorem, he has the knowledge ofthousands of theorems and definitions. He also knows how and when touse them. This is a very difficult process to automate. <p>Automatic and semi-automatic theorem proving programs which are ableto use the knowledge of other theorems and definitions are therebyable to reach arbitrarily far into formalizable mathematics and provecertain types of theorems. <p>The IPR program provides a method for storing and accessingmathematical knowledge so that an automated theorem proving programcan use it effectively. We hope this is a step in the rightdirection. <p>The report <!WA0><AHREF="file://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-127.ps">atp-127.ps</A>by Benjamin Shults reports on some work in this field. See the report<!WA1><ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-127a.ps">atp-127a.ps</a>for more clear description of the framework without the examples.<P>Since the publication of those papers, other challenges have appeared.If you are particularly interested in this work, then ask me aboutwork in progress.<p><hr><em>Do you have feedback or want more information? Contact </em><!WA2><ahref="http://www.ma.utexas.edu/users/bshults">Benjamin Shults</a>.<hr>⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -