An automated prover for Zermelo-Fraenkel set theory in Theorema

2Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.
Get full text

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.

Cite

CITATION STYLE

APA

Windsteiger, W. (2006). An automated prover for Zermelo-Fraenkel set theory in Theorema. Journal of Symbolic Computation, 41(3–4), 435–470. https://doi.org/10.1016/j.jsc.2005.04.013

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free