## CiME2

Evelyne Contejean, Benjamin Monate

LRI, Universite Paris-Sud, France

{contejea,monate}@lri.fr
### Architecture

CiME2 is intented to be a toolkit, which contains nowadays the following features:
- An interactive toplevel to allow naming of objects and call to
various functions.
- 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
criteria.

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.
### Implementation

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 http://cime.lri.fr/
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.
### Strategies

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 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 pairs. Each of these choices is given
a weight, and the lowest weighted choice is made. 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 to CASC, in the UEQ
division.
### References

- CiME2
- Contejean Evelyne, Marché Claude, Monate Benjamin, Urbain Xavier (2000),
**Cime version 2**,
Prerelease available at http://cime.lri.fr/
- CiME1
- 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.