Mathematica 9 is now available

Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

Gödel's Algorithm for Class Formation

Johan Gijsbertus Frederik Belinfante
Organization: Georgia Institute of Technology
Journal / Anthology

Automated Deduction - Cade-17
Year: 2000
Volume: LNCS 1831
Page range: 132-47

A computer implementation of Gödel's algorithm for class formation in Mathematica is useful for automated reasoning in set theory. The original intent was to forge a convenient preprocessing tool to help prepare input files for McCune's automated reasoning program Otter. The program is also valuable for discovering new theorems. Some applications are described, especially to the definition of functions. A brief extract from the program is included in an appendix.

*Mathematics > Foundations of Mathematics > Logic
Related items

*Reasoning About Iteration in Gödel's Class Theory   [in Articles]