The Theorema Project: A Progress Report
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru,
W. Windsteiger.
In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS
2000, Symposium on the Integration of Symbolic Computation and Mechanized
Reasoning, August 6-7, 2000, St. Andrews, Scotland, M. Kerber and M. Kohlhase
eds.), A.K. Peters, Natick, Massachusetts, pp. 98-113. (ISBN 1-56881-145-4.
Copyright: A.K. Peters.)
ABSTRACT:
We report on the progress made in the development of Theorema since
the first overview paper on Theorema (1997).
The main new features described are:
- the Theorema formal text language,
- the Theorema command language,
- the Theorema computational sessions,
- the PCS prover for proofs in elementary analysis and similar theories
in which concepts are defined by formulae with alternating universal
and existential quantifiers,
- semantical rewriting as a part of the PCS proof strategy,
- the call of algebraic solvers in the solve-phase of the PCS strategy,
- a set theory prover,
- methods for proof simplification,
- the Groebner bases prover for boolean combinations of equalities,
- the Gosper-Zeilberger-Paule prover for combinatorial identities.
The paper that can be downloaded is a slightl extension of the paper that
appeared in the above proceedings.