Automated Theorem Proving Group
[Note: This page contained information about the
Automated Theorem Proving group under the direction of Woody
Bledsoe. With the passing of Woody Bledsoe, this group no longer
exists. However, there is still a good bit of research in ATP
happenning at UT-Austin under the direction of Robert Boyer and J.
Moore. The information on this page is out of date.]
The Automated Theorem Proving group is part of the Computer Science and Mathematics departments at The University of Texas at
Austin.
We produce methods and systems intended to prove theorems in
first- and higher-order logic with the intention of applying these
systems and methods to problems primarily in mathematics, but also
in computer science and technology.
Here
is an index of electronically-available tech-reports from our
FTP site.
The ATP tech report series is not being continued currently. New
tech reports are being added to the AI Lab tech report
series.
Who are we?
Present group
Alumni
Others related to the group
What have we done?
- IMPLY
- The UT natural deduction prover
- STRIVE
- Larry Hines' First-order logic inequality prover.
- STRUVE
- Larry Hines' set theory prover.
- Chou's Geometry prover
- and various improvements thereto including McPhee's.
- SET-VAR
-
Precondition Prover
- NQTHM
- Boyer and Moore's prover developed at CLInc.
- This is an incomplete list.
What are we doing now?
- IPR
- This is an incomplete list.
Do you have feedback or want more information? Contact Benjamin Shults.