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.
Mendeley saves you time finding and organizing research
Choose a citation style from the tabs below