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