RISC JKU

The Set Theory Prover

The Theorema set theory prover is also based on the PCS principle. In addition to the predicate logic natural deduction inference rules it incorporates special inference rules for the basic notions of set theory, in particular the special set quantifiers.

Classes of Equivalence: Definitions
[Graphics:../Images/index_gr_22.gif]
[Graphics:../Images/index_gr_23.gif]
[Graphics:../Images/index_gr_24.gif]
[Graphics:../Images/index_gr_25.gif]
[Graphics:../Images/index_gr_26.gif]
A Proof
[Graphics:../Images/index_gr_27.gif]
[Graphics:../Images/index_gr_28.gif]

                        [Graphics:../Images/index_gr_29.gif] show


Converted by Mathematica      June 17, 2002