Proving Theorems of Type Theory Automatically with TPS

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 20

Intelligent Systems Demonstrations

Automated reasoning can be expected to play a significant role in many applications of artificial intelligence, and techniques for proving theorems automatically can serve as inference mechanisms in general purpose automated reasoning tools. We demonstrate and discuss how the TPS automated Theorem Proving System proves theorems of type theory, which is also known as higher-order logic and includes first-order logic. Notations used by TPS, which are very close to traditional notations of logic and mathematics, are explained. In a practical sense, type theory is a richer and more expressive formal language than first-order logic. A great variety of statements can be expressed very naturally in type theory, though most of the theorems which TPS has proved automatically thus far have a mathematical flavor. Examples include: X5305: Cantor’s Theorem that every set has more subsets than members. 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.