RISC RISC Research Institute for Symbolic Computation  
  • @inproceedings{RISC314,
    author = {W. Windsteiger},
    title = {{An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema}},
    booktitle = {{Logic, Mathematics and Computer Science: Interactions (LMCS 2002)}},
    language = {english},
    abstract = {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 ``Prove-Compute-Solve''-paradigm as its major strategy for generating proofs in a natural style for statements involving constructs from set theory.},
    pages = {266--280},
    address = {RISC, Schloss Hagenberg, Austria},
    isbn_issn = {ISBN 3-902276-03-7},
    year = {2002},
    month = {October},
    note = {Symposium in Honor of Bruno Buchberger's 60th Birthday, Appears in RISC-report Series Nr. 02-60},
    editor = {K. Nakagawa},
    refereed = {yes},
    length = {15}