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.
Windsteiger, W. (2006). An automated prover for Zermelo-Fraenkel set theory in Theorema. Journal of Symbolic Computation, 41(3–4), 435–470. https://doi.org/10.1016/j.jsc.2005.04.013