CiME : Completion Modulo E


Completion algorithms are used for computing canonical rewrite systems for equational specifications. Completion modulo a theory E allows to build-in some theories E, but until now the only case seeming useful is when E is the associativity and commutativity of some operators. One problem arising when using such a technique with other E such ACU (AC+unit), ACI (AC+idempotency), groups theory, etc.; is that rewriting on E-congruence classes does not terminate in general. Another problem is the unification process, which has to be done modulo E. These difficulties have been solved by the use of a new rewrite relation: E-normalised rewriting, and a corresponding completion algorithm has been designed.

The background theory is explained in the LICS'94 article (extended abstract) Normalised rewriting and normalised completion and in the JSC article (full paper) Normalized Rewriting: an alternative to Rewriting modulo a Set of Equations.

CiME is developed in our research team DÉMONS, the main author is Claude Marché, with contributions of Evelyne Contejean , Ralf Treinen, Emmanuel Engel, Florent Jacquemard, Hubert Comon.

The development of CiME is supported in part by the EU project CCL, the HCM Network SOL, the HCM Network CONSOLE, the « GDR de programmation du CNRS », and a cooperation between the CNRS and the JNICT (project 4312).

Current state of development

The last release is CiME 1.15 alpha, dated September 30, 1997. It is an alpha version that have several known bugs, see below. Several new things have been added since this version, and there will be no CiME 1.15 version. The next release will be numbered 2.0 and will include several improvements including :


CiME is written in Objective CAML, a functional language of the ML family developed in the CRISTAL project at INRIA Rocquencourt.

CiME also uses the very fast AC-matching algorithm written by Steven Eker from the PROTHEO project at INRIA-Lorraine.

Last modification of this page: may 19, 1999
To DÉMONS home page