**Can ELAN run under LINUX?**ELAN runs under Linux on PC machines. Look at How to get ELAN

**Can ELAN run on Windows9* or NT?**Not yet fully. We have already a first port of the interpreter to NT, but we do not distribute it currently. If you are interested in getting a preliminary NT version or in contributing to porting it, do not hesitate to contact us (elan@loria.fr).

**Is ELAN devoted to prototyping constraint solvers?**We made many implementations of constraint solvers using ELAN, and the use of the strategy languages is extremely useful to describe the behavior of the solvers. But ELAN is by no mean devoted to this specific objects, and many other applications have been programmed in the language, see

. **What is the relationship with CHR?**Constraint Handling Rules introduced by Thom Fruewirth is a language devoted to the description of constraint manipulation rules, initialy designed as an extention of the constraint logic programming system Eclipse. ELAN has also been used to program constraint manipulations. Interests of ELAN over CHR are the semantics of ELAN (either rewriting calculus or logic), the possibility to use strategies (either deterministic or not), the possibility to use associative-commutative operators, and that rewrite rules and strategies are compiled very efficiently. One nice feature of CHR is to have constraints as a first class concept, which is not currently the case in ELAN.

**Does ELAN need the term rewrite systems it implements to be confluent and terminating?**In an ELAN program, the set of rules is splitted in two main parts: labelled and unlabelled rules. The set of unlabelled rules is assumed to be confluent. On the set of labelled rules no hypothesis is made and it is perfectly OK to have for example the rule

*[identity] x -> x***Is ELAN using backtracking?**Yes this is the fundamental mechanism used for implementing dk (don't know) first and dc (don't care) strategies. It is implemented particularly efficiently and documented in CPL a Choice Point Library

**What is the relationship between ELAN and LCF, specificaly, the way rewriting is defined and used in LCF?**A first important difference is that the underlying calculus of ELAN is the rewriting calculus: i.e. rewriting plus strategies. In LCF, the primarily calculus is the lambda calculus. The following excerpt from A Higher-Order Implementation of Rewriting enlight the relationship between LCF and ELAN. It situates also the general research direction on the rewriting calculus.

*``LCF is used not only for performing particular proofs, but also for research into proof techniques. The programming language ML provides the flexibility needed for this research. The discovery of the operators THEN, ORELSE, and REPEAT, for combining tactics, was a breakthrough in the development of Edinburgh LCF. So it is exciting to find similar operators for combining conversions, especially since tactics and conversions have little else in common. This calls for an inquiry into instances of this programming style.''***What is the relationship between ELAN and MAUDE, developped at SRI?**

ELAN and MAUDE are both rule based languages that inherit in particular of the OBJ language and experience. From the language point of view, the main difference between the two languages is that ELAN as two first class concepts: Rules and Strategies. In Maude the first class concept are Rules and strategies are reached via the reflective capability of rewriting logic. From the system point of view, the main difference is that MAUDE has a very efficient interpreter as ELAN has an interpreter as well as a very efficient compiler. See this page on related systems for more details.