=ADD=
=reftype=
14
=number=
00-37
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/2000/00-37.ps.gz
=year=
2000
=month=
05
=author=
Buchberger; B. + Vasaru; D. + Jebelean; T.
=title=
The Theorema System: Current Status and the Proving-Solving-Computing Cycle
=abstract=
The Theorema project aims at supporting, within one consistent logic and
one coherent software system, the entire mathematical exploration cycle
including the phase of proving.

We summarize the main features of the Theorema system: 
the formal text language,
the computational sessions,
propositional and predicate-logic proving,
proving by induction and by simplification,
the set theory prover,
special provers (Groebner Bases, Zeilberger, external),
the cascade-meta-strategy for the  \TxTma\  provers,
proof simplification,
and the Prove-Compute-Solve (PCS) prover.
We discuss in more detail the PCS prover which is based on a combination
of techniques for predicate-logic proving, rewriting using universal formulae,
and solving in specific domains using black-box engines.
=sponsor=
FWF SFB P1302, INTAS 76-960, Land Ober\"osterreich project Prove.
=howpublished=
RTETP 2000: Rewriting Techniques and Efficient Theorem Proving, Kiev, Ukraine, May 2000.