CiME 2 and CASC 18
E. Contejean, B. Monate
LRI, Universite Paris-Sud, France
CiME is intended to be a toolkit, which contains nowadays the following
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.
- An interactive toplevel to allow naming of objects and call to
- Solving Diophantine constraints over finite intervals
- Solving Presburger constraints
- String Rewriting Systems, KB completion.
- Parameterized String Rewriting Systems confluence checking
- Term Rewriting Systems, possibly with commutative or
associative-commutative symbols, KB or ordered completion.
- Termination of TRSs using standard or dependency pairs criteria,
automatic generation of termination orderings based on polynomial
interpretations, including weak orderings for dependency pairs
CiME2 is fully written in
Objective CAML, a functional language of the ML family developed in the
CRISTAL project at
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
As special tool named
tptp2cime 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:
- The first one is, given an equation, how to choose its orientation
when it becomes a rule?
The choice is made thanks to an ordering which has usually to be
provided by the user.
During the competition, this ordering is arbitrarily fixed to be an
RPO ordering based on a precedence where the symbols are ordered
according to their arities.
- The second one is which inference rule has to be applied to the
system, among orienting an equation into a rule and computing critical
Each of these choices is given a weight, and the lowest weighted choice
The weight depends on the size of the involved equations/rules and
on how "old" they are.
Some tuning may occur at this point by choosing the ratio between the
coefficients for the size and the age.
During the competition, this ratio will be fixed.
Expected Competition Performance
This will be the first participation of CiME2 in CASC, in the UEQ division.
Acknowledgments: Claude Marché and Xavier Urbain contributed to the
development of CiME 2.
- Contejean E., Marché C., Monate B., Urbain X. (2000),
CiME version 2,
- Contejean E., Marché C. (1996),
CiME: Completion Modulo E,
Proceedings of the 7th International Conference on Rewriting
Techniques and Applications
(New Brunswick, USA),
Lecture Notes in Computer Science 1103,