=ADD=
=reftype=
14
=number=
99-42
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1999/99-42.ps.gz
=year=
1999
=month=
12
=author=
Buchberger; Bruno + Dupre; Claudio + Jebelean; Tudor + Kriftner; Franz + Nakagawa; Koji + Vasaru; Daniela + Windsteiger; Wolfgang
=title=
Theorema: A Progress Report
=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. In this paper we report on some of the new
features of Theorema that have been designed and implemented since the first
expository version of Theorema in 1997. These features are:
 - the Theorema formal text language
 - the Theorema computational sessions
 - the Prove-Compute-Solve (PCS) prover of Theorema
 - the Theorema set theory prover
 - special provers within Theorema
 - the cascade meta-strategy for Theorema provers
 - proof simplification in Theorema
In the conclusion, we formulate the design goals for the next version of
Theorema
=howpublished=
Submitted to ISSAC 2000.
=sponsor=
SFB/FWF project F1302
=keywords=
automatic reasoning