An automated prover for Zermelo-Fraenkel set theory in Theorema

This paper presents some fundamental aspects of the design and the implementation of an automated prover for Zermelo-Fraenkel set theory within the well-known Theorema system. The method applies the "ProveCompute-Solve"-paradigm as its major strategy for generating proofs in a natural style for statements involving constructs from set theory.

• Type: Journal
• Year: 2006
• Where: JSC
• Authors: Wolfgang Windsteiger
• Keywords: Automated Prover, Fundamental Aspects, JSC 2006, Well-known Theorema