Wolfram Library Archive

Courseware Demos MathSource Technical Notes
All Collections Articles Books Conference Proceedings

Equational Prover of THEOREMA

Temur Kutsia
Organization: Research Institute for Symbolic Computation
Department: Johannes Kepler University
Journal / Anthology

Rewriting Tecniques and Applications, Proceedings
Year: 2003
Page range: 367-379

The equational prover of the THEOREMA systems is described. It is implemented on Mathematica and is designed for unit equalities in the first order or in the applicative higher order form. A (restricted) usage of sequence variables and Mathematica built-in functions is allowed.

*Wolfram Technology > Application Packages > Additional Applications > Theorema