Theorema: Extending Mathematica by Automated Proving

Bruno Buchberger

Invited talk at PrimMath 2001 (The Programming System Mathematica in 
Science, Technology, and Education), University of Zagreb, Electrotechnical
and Computer Science Faculty, September 27-28, 2001. In: Proceedings 
edited by D. Bosanac, D. Ungar, pp.10-11, long version on CD. 
(ISBN 953-6076-71-3.)




ABSTRACT:


This is a quick but comprehensive introduction into Theorema, which 
illustrates the main features of Theorema by examples:

- Theorema formal text including logicographic symbols

- the PCS prover (example limit theorem)

- the set theory prover (example: theorem on equivalence classes)

- the induction prover and the cascade (example: commuativity of 
  addition)

- the Groebner bases prover (example: boolean combinations
  of equalities over the complex numbers)

- the Paule-Schorn combinatorial identities prover 
  (example: the SIAM problem)

- computation and functors in Theorema (example: polynomial
  domains)