Set theory in first-order logic: Clauses for Gödel's axioms (Q1097252)

In this paper we present a set of clauses for set theory, thus developing a foundation for the expression of most theorems of mathematics in a form acceptable to a resolution-based automated theorem prover. Because Gödel's formulation of set theory permits presentation in a finite number of first-order formulas, we employ it rather than that of Zermelo- Fraenkel. We illustrate the expressive power of this formulation by providing statements of some well-known open questions in number theory, and give some intuition about how the axioms are used by including some sample proofs. A small set of challenge problems is also given.