Automated Deduction in Set Theory

摘要

Phase II of the project extended the framework for automated theorem proving in set theory developed in Phase I, and implemented it in a theorem-proving system written in the Prolog language. The goals of the project were: (1) to explore the idea of using diagrams as a means of guiding automated proofs, (2) to obtain powerful methods of choosing relevant objects within automated proofs, and (3) to develop a theorem-proving system for set theory employing these techniques. The key results are four non-trivial theorems which can be proved with the software. Researchers developed two theorem-proving systems: (1) a syntax-based theorem prover for set theory, and (2) GROVER, a more semantically oriented graphical prover built on top of (1). With the first, they obtained fully automated proofs of Cantor's Theorem, Transfinite Induction, and Transitive Closure Interpolation. With GROVER, building on the latter two proofs, they obtained an automated proof of the Diamon Lemma from a diagram. In addition, GROVER provides an extensible framework for the mathematician to explore other proofs in an interactive graphical language.