http:^^www.ma.utexas.edu^users^bshults^atp^

来自「This data set contains WWW-pages collect」· EDU^USERS^BSHULTS^ATP^ 代码 · 共 137 行

EDU^USERS^BSHULTS^ATP^
137 行
字号 
Date: Mon, 06 Jan 1997 19:51:00 GMTServer: NCSA/1.4.2Content-type: text/html<html><TITLE>Automated Theorem Proving Group</TITLE><body    bgcolor="#ffffff"  text="#000000"  link="#0000ee" vlink="551a8b" alink="ff0000"><H1>Automated Theorem Proving Group</H1>The Automated Theorem Proving group is part of the <!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><!WA0><ahref="http://www.cs.utexas.edu/">Computer Science</a> and <!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><!WA1><ahref="http://www.ma.utexas.edu/">Mathematics</a> departments at <!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><!WA2><aHREF="http://wwwhost.cc.utexas.edu">The University of Texas atAustin</a>.<p>We produce methods and systems intended to prove theorems in first-and higher-order logic with the intention of applying these systemsand methods to problems primarily in mathematics, but also in computerscience and technology.<p><h4><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><!WA3><ahref="ftp://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/INDEX.html">Hereis an index</a> of electronically-available tech-reports from our <!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><!WA4><ahref="ftp://ftp.cs.utexas.edu/pub/bshults">FTP site</a>.</h4><p>The ATP tech report series is not being continued currently.  New techreports are being added to the <!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><!WA5><ahref="http://www.cs.utexas.edu/users/ai-lab/">AI Lab</a> tech reportseries.<p><h2>Who are we?</h2><h3>Present group</h3><ul><li>Larry Hines<li><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><!WA6><a href="http://www.cs.utexas.edu/users/martym">Marty Mayberry</a><li><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><!WA7><a href="http://www.ma.utexas.edu/users/bshults">Benjamin Shults</a></ul><h3>Alumni</h3><ul><li><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><!WA8><ahref="http://www.ma.utexas.edu/users/bshults/ATP/bledsoe-studs.html">Previous Students of Woody Bledsoe.</a><li><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><!WA9><a href="http://www.ma.utexas.edu/users/bshults/ATP/boyer-studs.html">Previous Students of Robert Boyer.</a><li><em>This is an incomplete list.</em></ul><h3>Others related to the group</h3><ul><li>The late Woody Bledsoe<!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><!WA10><aHREF="http://www.cs.utexas.edu/users/UTCS/report/1994/profiles/bledsoe.html">(His computer science faculty profile.)</a><li><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><!WA11><a href="http://www.cli.com/staff/resumes/boyer">RobertBoyer</a><li><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><!WA12><a href="http://www.cli.com/staff/resumes/moore">J Strother Moore</a><li><em>This is an incomplete list.</em></ul><h3><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><!WA13><a href="http://www.ma.utexas.edu/users/bshults/ATP/visitors.html">Past visitors and collaborators</a></h3><h2>What have we done? </h2><ul><li>IMPLY<ul><li>The UT natural deduction prover</ul><li>STRIVE<ul><li>Larry Hines' First-order logic inequality prover.</ul><li>STRUVE<ul><li>Larry Hines' set theory prover.</ul><li>Chou's Geometry prover<ul><li>and various improvements theretoincluding McPhee's.</ul><li><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><!WA14><ahref="file://ftp.cs.utexas.edu/pub/bshults/papers/SET-VAR-JAR-11.ascii">SET-VAR</a> <ul>  <li>Feng's prover for set theory<li><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><!WA15><ahref="file://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-119.ascii">Implementation description</a> <li><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><!WA16><ahref="file://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-120.ascii">Proof of Heine-Borel theorem</a></ul><li><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><!WA17><ahref="file://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-116.tex">Precondition Prover</a><ul><li>Bledsoe's prover for analogy  <li><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><!WA18><ahref="file://ftp.cs.utexas.edu/pub/bshults/ATP-tech-reports/atp-124.ascii">Proof of the Heine-Borel theorem</a></ul><li><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><!WA19><a href="ftp://ftp.cli.com/pub/nqthm">NQTHM</a><ul><li>Boyer andMoore's prover developed at <!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><!WA20><a href="http://www.cli.com">CLInc.</a></ul><li><em>This is an incomplete list.</em></ul><h2>What are we doing now?</h2><ul><li><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><!WA21><ahref="http://www.ma.utexas.edu/users/bshults/IPR/atp.html">IPR</a><ul><li>Shults' <!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><!WA22><ahref="http://www.ma.utexas.edu/users/bshults/IPR/knowledge-using.html">knowledge-using</a> prover for mathematics.</ul><li><em>This is an incomplete list.</em></ul><h2><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><!WA23><ahref="http://www.ma.utexas.edu/users/bshults/ATP/related-links.html">RelatedLinks</a></h2><hr><em>Do you have feedback or want more information?  Contact </em><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><!WA24><ahref="http://www.ma.utexas.edu/users/bshults">Benjamin Shults</a>.<hr>

http:^^www.ma.utexas.edu^users^bshults^atp^ - 源码说明

本页面展示了「This data set contains WWW-pages collected from computer science departments of various universities」中的 http:^^www.ma.utexas.edu^users^bshults^atp^ 源码文件，采用 EDU^USERS^BSHULTS^ATP^ 编程语言编写，共 137 行代码。您可以在线阅读完整代码内容，也可以返回资源详情页下载完整源码包进行本地学习和开发。

虫虫下载站收录了大量与universities相关的技术资源，包括源代码、技术文档、电路图等，是电子工程师和嵌入式开发者的专业学习平台。

⌨️ 快捷键说明

复制代码Ctrl + C
搜索代码Ctrl + F
全屏模式F11
增大字号Ctrl + =
减小字号Ctrl + -
显示快捷键?