Evelyne Contejean, Benjamin Monate
LRI, Universite Paris-Sud, France


CiME2 is intented to be a toolkit, which contains nowadays the following features: The ordered completion of term rewriting systems will be used during the competion to attempt to solve unification problems, that is problems in the UEQ division.


CiME2 is fully written in Objective CAML, a functional language of the ML family developed in the CRISTAL project at INRIA Rocquencourt. CiME2 is available at as binaries for SPARC workstations running Solaris (at least version 2.6) and for pentium PCs running Linux, and its sources are available by read-only anynomous CVS.


There are two distinct kinds of strategies to perform completion:

Expected Competition Performance

This will be the first participation of CiME2 to CASC, in the UEQ division.


Contejean Evelyne, Marché Claude, Monate Benjamin, Urbain Xavier (2000), Cime version 2, Prerelease available at
Contejean Evelyne, Marché Claude (July 1996), CiME: Completion Modulo E, Ganzinger Harald, International Conference on Rewriting Techniques and Applications (New Brunswick, NJ, USA), pp.416-419, Lecture Notes in Computer Science 1103, Springer-Verlag.

Acknowledgments: Claude Marché and Xavier Urbain contributed to the development of CiME2.