CiME 2 and CASC 18

CiME 2

E. Contejean, B. Monate
LRI, Universite Paris-Sud, France


CiME is intended 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. As special tool named
handles the TPTP syntax instead of the standard CiME 2 syntax. tptp2cime is available as The sources for the competion is available here.


There are two distinct kinds of strategies to perform completion:

Expected Competition Performance

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


Contejean E., Marché C., Monate B., Urbain X. (2000), CiME version 2,
Contejean E., Marché C. (1996), CiME: Completion Modulo E, Ganzinger H., Proceedings of the 7th International Conference on Rewriting Techniques and Applications (New Brunswick, USA), pp.416-419, Lecture Notes in Computer Science 1103, Springer-Verlag.
Acknowledgments: Claude Marché and Xavier Urbain contributed to the development of CiME 2.
Benjamin Monate

Best Viewed With Any Browser 16/10/2003 (formatted with yamlpp).