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 semiautomatically 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, semiautomatically, and automatically. In automatic mode, TPS uses procedures for instantiating quantifiers on higherorder variables, strategies for mating literals, and higherorder 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:
