Ernest Schimmerling

Mathematical logic seminar - September 9, 2004

Time: 12 - 1:15 p.m.

Room: 150 Baker Hall

Speaker:     Peter Andrews   
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:

  • THM15B: If some iterate of a function f has a unique fixed point, then f has a fixed point.
  • THM136: The transitive closure of a relation is transitive.
  • THM145B: In a complete lattice, every monotone function has a fixed point.
  • THM531E: A subset of a finite set is finite.