Automated deduction in von Neumann-Bernays-Gödel set theory (Q1187858)

This article is a journal version of the author's thesis, which has been published as a book [Automated development of fundamental mathematical theories, Automated Reasoning Series, Kluwer (1993)]. The objective of the work was to find an axiomatization of set theory suitable to treat with first-order predicate logic theorem provers. To this end a clausal version of the von Neumann-Bernays-Gödel axiomatization of set theory was developed and over 400 theorems were proved using the resolution-based automated theorem prover Otter. A number of heuristics and tricks are presented for guiding a theorem prover and proving quite complex theorems, including Cantor's theorem, at least semiautomatically.