Wolfgang Windsteiger,
"An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema"
, in Journal of Symbolic Computation, Vol. 41, Nummer 3-4, Elsevier, Seite(n) 435-470, 2006, ISSN: 1095-855X
Original Titel:
An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema
Sprache des Titels:
Englisch
Original Kurzfassung:
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
Forschungs-