| Time: | 12 - 1:15 p.m. |
| Room: |
150 Baker Hall
|
| Speaker: |
Peter Andrews Professor Department of Mathematical Sciences Carnege Mellon University |
| Title: |
Proving theorems automatically and semi-automatically with TPS
|
| Abstract: |
Automated deduction has many potential applications, including
checking proofs in mathematical papers, verifying software and
hardware, and providing inference mechanisms for automated reasoning
tools. We demonstrate how the automated theorem proving system TPS
proves theorems of type theory. Proofs in TPS are expressed in
notations which are easy to read, and are very close to the
traditional notations of mathematics.
TPS can be used to construct formal proofs interactively, semi-automatically, and automatically. In automatic mode, TPS uses procedures for instantiating quantifiers on higher-order variables, strategies for mating literals, and higher-order unification to search for an expansion proof of the theorem to be proved. An expansion proof expresses in a nonredundant way the fundamental combinatorial structure underlying various proofs of the theorem. TPS then transforms the expansion proof into a proof in natural deduction style. Some examples of theorems which TPS can prove automatically are:
|