This document is available by FTP in various formats. It was converted to HTML using Hyperlatex 2.5.
We consider in this paper the problem of executing some CASL specifications thanks to the rewrite engine provided by the ELAN system, that implements rewriting in a very efficient way. The class of CASL specifications we are able to handle is precisely described. These algebraic specifications consist of many-sorted equational axioms (including possibly associative-commutative operators), where the equality predicate is used to express the congruence on terms whilst the equivalence connective allows us to define the congruence on boolean expressions built over predicates. Subsorting and partiality features are not considered in this framework, but we we deal with both basic and structured CASL specifications. The mapping from CASL to ELAN is performed by translating a CASL abstract syntax into the abstract syntax developed for ELAN. Our current implementation needs the CASL Tool Set developed in Bremen to parse a CASL specification and to generate the so-called "Fenv" abstract syntax, which is especially designed for connecting theorem-provers and deduction tools. By using our translation tool and then the ELAN compiler, we produce an executable program to perform computation of normal forms with respect to a given CASL specification.