 |
|
|
|
|
 |
|
|
Reasoning About Iteration in Gödel's Class Theory
|
|
|
|
|
|
| Organization: | Georgia Institute of Technology |
|
|
|
|
|
|
| Automated Deduction - Cade-19 |
|
|
|
|
|
|
A computer implementation of Gödel's algorithm for class for- mation in Mathematica was used to formulate definitions and theorems about iteration in Gödel's class theory. The intent is to use this approach for automated reasoning about a variety of applications of iteration using McCune's automated reasoning program Otter. The applications include the theory of transitive closures of relations, the arithmetic of natural numbers, construction of invariant subsets, and the Schröder-Bernstein theorem.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
http://www.math.gatech.edu/~belinfan/research/
|
|
For the newest resources, visit Wolfram Repositories and Archives »
