The CiME 1.15 alpha distribution
What's New ?
Since last release (1.13), the following points have been added or
changed :
- Unification :
E-unification is now available for E=ACUN. Several bugs in
E-unification, reported by Miki Hermann, have been corrected.
- Inductive reducibility test using automata techniques.
- Completion :
- Ordered Completion now available.
- Inductive Completion available.
- New orderings available :
- Orderings by polynomial interpretations have been generalized
to any minimum value mu, and are much faster.
- Building a new ordering from an old one via recursive program
scheme interpretations.
- Clever termination check via dependency pairs.
- Other bugs corrected :
Known bugs
This alpha distribution has known bugs, which will be fixed for the
next release. Due to large modifications that have been recently done,
the next release available would be numbered 2.0.
- Weak orderings : CiME allows now the definition of weak reduction
orderings, that is are not strictly monotonic. Such orderings are enough for proving termination of a system by the dependency pairs criterion. However, they should not be used for classical termination proofs or completion. But it is not checked.
- In case of failure of the dependency pairs criterion, there is a
bug in printing the non-decreasing dependency pairs: the wrong ones
are displayed,
- In some very rare cases, non ordered rules may appear even without
the -ordered option.
- The dependency pairs criterion still have some bugs in presence of
AC operators, due to a wrong computation of extended pairs. Thus
beware that in somme CiME may tell you that a system is terminating
whereas it is not.
Last modification of this page: May 20, 1998
Back to CiME home page