An automated prover for Zermelo-Fraenkel set theory in Theorema

  • Windsteiger W
  • 4

    Readers

    Mendeley users who have this article in their library.
  • 2

    Citations

    Citations of this article.

Abstract

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.

Author-supplied keywords

  • Automated theorem proving
  • Set theory
  • Theorema

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document

Authors

  • Wolfgang Windsteiger

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free