ELAN - Specification and Prototyping with Rules and Strategies
by Hélène Kirchner
The ELAN system is an environment for specifying and prototyping
constraint solvers, theorem provers and deduction systems in general. It
also provides a framework for experimenting their combination. The ELAN
language is based on labelled conditional rewrite rules and on strategies
for controlling their application. ELAN is developed in the PROTHEO project,
common to INRIA, CNRS and Universities of Nancy.
The PROTHEO project aims at designing and implementing tools for program
specification and verification. In this context, we study various deduction
systems, with a particular emphasis on the combination of theorem provers,
constraints solvers and decision procedures. The ELAN system provides an
environment for specifying and prototyping deduction systems in a language
based on rules controlled by strategies.
We choose the simple and well-known paradigm of rewriting as the logical
framework in which deduction systems can be expressed and combined, and
as the evaluation mechanism of the language. In contrast to many existing
rewriting-based languages where the term reduction strategy is hard-wired
and not accessible to the designer of an application, ELAN provides a strategy
language to control rewriting. Evaluation of strategy application is itself
based on rewriting.
In ELAN a rewrite rule may be labelled, may have conditions and may
introduce local variables useful to apply strategies on subterms. The strategy
language offers primitives for sequential composition, iteration, deterministic
and non-deterministic choices of elementary strategies that are labelled
rules. From these primitives, more complex strategies can be expressed.
In addition the user can introduce new strategy operators and define them
by rewrite rules.
The distributed version of ELAN includes an interpreter and a compiler
written in C++, a library of standard programs, a user manual and examples
of applications.
Examples of applications developed in ELAN are the design of rules and
strategies for constraint satisfaction problems, theorem proving tools
in first-order logic with equality, the combination of unification algorithms
and of decision procedures in various equational theories. For more information
on ELAN, see http://www.loria.fr/equipes/protheo/PROJECTS/ELAN/elan.html
Please contact:
Hélène Kirchner LORIA-CNRS
Tel:+33 3 83 59 30 12
E-mail: Helene.Kirchner@loria.fr
