Summary: 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 biief extract from t biief extract from the program is included in an appendix.
For the entire collection see [Zbl 0939.00024].