=ADD=
=reftype=
14
=number=
01-14
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2001/01-14/
=year=
2001
=month=
07
=author=
Windsteiger; Wolfgang
=title=
A Set Theory Prover in Theorema: Implementation and Practical Applications
=abstract=
In this thesis we introduce the Theorema Set Theory prover, a
method for automatically generating proofs of statements involving
notions from set theory and its implementation in the Theorema
system. The method follows the known natural deduction paradigm for
automated theorem proving, which aims at generating mechanized proofs in
a style similar to human mathematicians. Moreover, the prover applies a
``Prove-Compute-Solve''-strategy, which has already been applied
successfully for generating proofs in elementary analysis, structuring
proofs into phases of
 - applying standard inference techniques from predicate logic (i.e. proving),
 - rewriting formulae using assumptions from the knowledge base (i.e. computing, simplifying), and
 - applying powerful methods from computer algebra for solving existentially quantified formulae (i.e. solving).
The entire method is implemented in the frame of the Theorema
system, whose most important principles will be outlined in order to
show the integration of set theory proving into the existing software
system. The power of the method is shown in many examples, organized
into entire explorations of mathematical theories based on the theory of
sets. These explorations also show the feasibility of Theorema's
approach to support the entire cycle of mathematical activities and, in
particular, the interplay between proving and computing in the same
language and the same underlying logic.
=note=
PhD Thesis
=sponsor=
FWF SFB F013, PROVE (Land O{\"O}), EU Calculemus (HPRN-CT-2000-00102)