|
|
|
|
|
|
|
|
Equational Prover of THEOREMA
|
|
|
|
|
|
Organization: | Research Institute for Symbolic Computation |
Department: | Johannes Kepler University |
|
|
|
|
|
|
Rewriting Tecniques and Applications, Proceedings |
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|