Computer Assisted Proofs in Set Theory

Belinfante's interest in computer assisted theorem proving has mainly concentrated on obtaining proofs of theorems in set theory using the first-order logic resolution-style theorem prover Otter, a powerful automated reasoning program developed by William McCune at Argonne National Laboratories.

Robert Boyer's idea of using Kurt Gödel's finite axiomatization of set theory is the basis for all Otter proofs of theorems in set theory. Art Quaife in his remarkable PhD thesis showed how to reduce the plethora of Skolem functions that had plagued earlier work, and listed several hundred theorems in set theory that he proved.

Belinfante explored the use of Otter for more advanced topics in set theory, including theorems about certain standard functions in set theory, cross products, ordinal number theory, equipollence, the theory of finite sets, partial ordering, transitive closure, and so on.

Otter Input Files, Proof Lists and Proof Summaries

Current version of Belinfante's GOEDEL program

Although the axiom scheme for unrestricted class formation must be abandoned to obtain a finite axiom system for set theory in first order logic, Gödel provided an algorithm for translating the usual constructions into the more restrictive ones needed in his formal system.

Belinfante implemented Gödel's algorithm in Mathematica to facilitate converting formulas of set theory to the formalism needed for proofs in Otter, adding thousands of simplification rules to obtain compact output. This program has evolved into a powerful tool for discovering and formulating facts which can be proved using Otter.


Links to some other sites.

Link back to Belinfante's vita.


If you have comments about anything here, please send me e-mail:
belinfan@math.gatech.edu


Modified: 2003 July 3