=ADD=
=author=
Buchberger; Bruno + Jebelean; Tudor + Kriftner; Franz + Marin; Mircea + Tomuta; Elena + Vasaru; Daniela
=title=
A Survey of the {\em Theorema} Project
=number=
97-15
=month=
3
=year=
1997
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1997/97-15.ps.gz
=abstract=
The {\em Theorema} project aims at {\em extending current computer
algebra systems by facilities for supporting mathematical proving}.
 The present early-prototype version of the {\em Theorema} software system is
 implemented in
{\em  Mathematica 3.0}.
  The system consists of a general higher-order predicate logic prov\-er
 and a {\em  collection of special provers} that call each other depending on
 the particular proof situations.
  The individual provers  {\em imitate the proof
 style of human mathematicians} and aim at
 {\em producing human-readable proofs in natural language} presented
 in {\em nested cells} that facilitate studying  the computer-generated
 proofs at various levels
 of detail.
 The special provers are {\em  intimately connected with the functors}
 that build up the various mathematical domains.
=howpublished=
Proceedings of ISSAC'97 (International Symposium on Symbolic and Algebraic Computation,
	Maui, Hawaii, July 21-23, 1997),
        W. Kuechlin (ed.),
        ACM Press 1997,
        pp. 384--391.
=location=
2
=owner=
2
=source=
3
=reftype=
14