SCS Undergraduate Thesis Topics
|Ian Kash||Wilfried Sieg||A Partially Automated Proof of the Cantor-Bernstein Theorem|
AProS is an automated proof search system created in the department of philosophy at Carnegie Mellon which finds natural deduction proofs for assertions in first order logic. A distinctive feature of AProS is that it produces natural proofs, similar to those a human might produce. I plan to extend AProS to use it to prove mathematical theorems from appropriate axioms, with the particular goal of proving the Schröder-Bernstein theorem from the axioms of Zermelo-Fraenkel set theory. Previous work has extended AProS to allow for metamathematical proofs (specifically proofs of Gödel's incompleteness theorems and related theorems), but this involved coding domain specific heuristics into the overall AProS architecture. I will implement appropriate general heuristics for handling axioms, definitions, and functions. I conjecture that when applied to the specific axioms and definitions of set theory, with appropriate lemmata, a proof of the Schröder-Bernstein theorem can be found. In keeping with the overall goals of the AProS project, this extension should generate natural proofs.