Reasoning about iteration in Gödel’s class theory. (English) Zbl 1260.68365
Baader, Franz (ed.), Automated deduction – CADE-19. 19th international conference on automated deduction, Miami Beach, FL, USA, July 28 – August 2, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40559-3/pbk). Lect. Notes Comput. Sci. 2741, 228-242 (2003).
Summary: A computer implementation of Gödel’s algorithm for class formation 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.
For the entire collection see [Zbl 1026.00022].
For the entire collection see [Zbl 1026.00022].
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B35 | Mechanization of proofs and logical operations |
