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

Abstract

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 theoren prover. Because Gödel's formulation of set theory permits presentation in a finite number of first-orde formulas, we employ it rather than that of Zermelo-Fraenkel. We illustrate the expressive power of thi 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 challeng problems is also given. © 1986, D. Reidel Publishing Company. All rights reserved.