An automated prover for Zermelo-Fraenkel set theory in Theorema

Abstract

This paper presents some fundamental aspects of the design and the implementation of an automated prover for Zermelo-Fraenkel set theory within the Theorema system. The method applies the "Prove-Compute-Solve" paradigm as its major strategy for generating proofs in a natural style for statements involving constructs from set theory. © 2005 Elsevier Ltd. All rights reserved.