Previous Page

ELAN - Applications

Many computational processes in automated deduction can be expressed as instances of a general schema that consists of applying transformation rules on formulas with some strategy, until reaching specific normal forms. Such processes are naturally modelised in ELAN. Several applications have been designed and are classified according to the area of interest, namely programming, proving and solving.

Programming: One of the first application was to prototype the fundamental mechanisms of logic and functional programming languages like first-order resolution and -calculus. The general framework of Constraint Logic Programming  can be easily designed in the ELAN framework [19], since its operational semantics is clearly formalised as rewrite rules, although the application strategy is often defined in an informal way. Some implementations  [22] related to a calculus of explicit substitutions (the first-order rewrite system that mimics -calculus) open the way of implementing higher-order logic programming languages via a first-order setting. Another calculus of explicit substitutions based on the -calculus is used to provide a formal specification of Input/Output for ELAN [23].

Proving: ELAN was used in order to implement a predicate prover based on the rules proposed by J.-R. Abrial, and implemented in the B-tools . We developed also a propositional sequent calculus, completion procedures for rewrite systems [24]. A library for automata construction and manipulation has been designed. Approximation automata are used to check conditions for reachability, sufficient completeness, absence of conflicts in systems described by non-conditional rewrite rules [25].

Solving: The notion of rewriting controlled by strategies is used in  [21] to describe in a unified way the constraint solving mechanism as well as the meta-language needed to manipulate the constraints. This provides programs that are very close to the proof theoretical setting used now to describe constraint manipulations like unification or numerical constraint solving. ELAN offers a constraint programming environment where the formal description of a constraint solver is directly executable. ELAN has been tested on several examples of constraint solvers for various computation domains and combinations like abstract domains [21][27] (term algebras) and more concrete ones (booleans, integers, reals). In [28][29][30][31], it is shown how to use computational systems as a general framework for handling Constraint Satisfaction Problems (CSP for short). The approach leads to the design in ELAN of COLETTE, a solver for constraints over integers and finite domains.