 |
|
|
|
|
 |
|
|
Gödel's Algorithm for Class Formation
|
|
|
|
|
|
| Organization: | Georgia Institute of Technology |
|
|
|
|
|
|
| Automated Deduction - Cade-17 |
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
http://www.math.gatech.edu/~belinfan/research/
|
|
For the newest resources, visit Wolfram Repositories and Archives »
