From a Computer Algebra Library to a System with an Equational Prover - Artificial Intelligence and Symbolic Computation - page 282

On Languages: Haskell is chosen as the implementation language ( IL ); the
prover is written in IL, and it reasons about specifications expressed in OL. The
prover strategies are formulated in the strategy language ( SL ), for which we have
again found Haskell to be adequate. When OL develops a sucient richness, it
has the potential to become an SL.
Whydonotwechooseaprovertoolfromagreatnumberofexistingones?
After one year of investigation we failed to find a tool satisfying our requirements
(and personal taste): (1) being open source, (2) having sucient OSTRW to be
an OL, (3) providing a good high-level functional language for implementation,
and suitable universality for a strategy language, (4) having a rich CA library
and TRW library ( Maude was candidate No. 1). And our taste also does matter:
an encouraging six-year experience with Haskell , with its “laziness”, clarity and
a balance between its being high-level and the eciency of the Glasgow Haskell
tool, with implementing in it a large CA library (to link to the prover) - all impel
us to continue in this direction. As a more distant perspective, we intend the
future OL to become a really adequate language for expressing strategic-level
knowledge in programs.

Illustrating the System with an Example.
The following simple problem is taken from Example 3.7 in [2]. Let G be a group
with operations e, *, i ,and P a non-empty subset in G such that if X and
Y belong to P then X*(i Y) belongs to P . Prove that it follows from these
axioms that (1) e ∈ P , (2) for all X(X ∈ P ==> i X ∈ P)
To solve this problem, denote x ∈ P as (P x) and specify a theory as a

many-sorted specification in OL:

groupTask = theoryUnion (bool lpo) groupWithP
where
groupWithP =
Theory {sorts = [G],
operators = [e : -> G, i_: G -> G, -- inversion

_*_: G G -> G, P_: G -> Bool], -- for subset

variables = [[X, Y, Z] : G],
equations = [(X*Y)*Z = X*(Y*Z), -- Group

e * X = X, (i X)*X = e], -- laws

opPrecedence = preced, greaterTerm = (lpo preced)

btLaws = [], btOrdering = ... }

preced = [P, i, *, e, false], -- P > i > ...

This specification is expressed as an IL data. The TRW interpreter treats
such specifications as direct term reduction programs. Other parts of the prover,
like completion , treat it as a theory from which to derive the consequences. The
term ordering ( greaterTerm ) has the operator precedence table as a parameter.
theoryUnion is a function joining theories in a sensible way; here it joins the
theory for Boolean algebra. This example is processed by the prover, with the
result printed to a string, by the following IL program: