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
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
- Belinfante uses a standard
input file STANDARD.IN for all Otter proofs in set theory. This file needs
only to be modified by replacing the set of support (sos) list with the
negated statement of the theorem to be proved and adjusting assignments of
various Otter parameters, especially weights of terms expected to occur in the
proof. The output file STANDARD.OUT contains the statements of most theorems
proved to date using Otter, but it omits lemmas and subsumed theorems.
- All current versions of the usable
lists and demodulator
lists loaded by include statements in the standard input file are available
here. These lists are updated as new theorems are proved.
- The log
files, documenting the order in which theorems were added to the standard
- From the compact proof
summary files prepared for each theorem, one can see the previous theorems
that Otter selected for each proof, and the actual proof that Otter obtained.
In addition, these *.SUM files contain revealing statistics about each proof.
There are proof summaries also for lemmas not included in the standard usable
and demodulator lists, and for alternate proofs of some theorems. Text files
provide comments about how the proofs were found. The ALL.POS files, which
were used to prepare the standard lists, ask Otter to automatically discard
subsumed lemmas and to discover which equations can be made into demodulators
and how to orient them, based on a specified lex order. The output from the
ALL.POS files are in the ALL.CLS files. The order in which the theorems are
listed in the standard lists was determined by studying the PROOFUSE.TXT files
which document the interdependence of the theorems within each group. The
STUDYALL.TXT files were used to determine in what order the various different
groups should be arranged in the STANDARD.IN file.
- Frequently used Perl
scripts (for a non-Unix machine) include SUMMARY.PL, used to automatically
extract proof summaries from Otter output files and ALL2USE.PL to extract
usable lists from the ALL.CLS files.
- Link to Derrick Coetzee's Lisp program po2hr for converting
Otter proof objects to human-readable LaTeX form.
- PDF file comparing Kurt Gödel's notation with the
notation used by Quaife and Belinfante.
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.
- Current version of the GOEDEL
file of Belinfante's paper, "On a Modification of Gödel's Algorithm for
Class Formation," Association for Automated Reasoning News Letter, No. 34, pp.
10-15, October, 1996.
- Standard suites
used to test the GOEDEL program.
- Some tools
for discovering new theorems.
- Sample Mathematica notebooks
illustrating how the GOEDEL program can be used. Note: Some notebooks load
prior versions of the GOEDEL program, leading to the discovery of new rules
that have been incorporated into the current version.
- Some logs
of Mathematica sessions.
Links to some other sites.
Link back to Belinfante's vita.
If you have comments about anything here, please send me e-mail:
Modified: 2003 July 3