The CiME 1.13 distribution
Please read the documentation for installation instructions.
What's New ?
Since last release (1.05), the following point have been added or
- Unification :
E-unification is now available for E=ACU,AG and BR. Both plain and
AC-complete forms, as defined in (Boudet, Contejean &
(implemented by Evelyne
- Completion :
- Completion strategy completed changed, due to AC-complete
- Critical pair criterion "blocking" implemented.
- Syntactic sugar :
- postfix operators.
- enhanced pretty-printing (implemented by Florent Jacquemard).
- more statistics.
- New classes of problems to solve :
- conjectures, to be solved during completion.
- unification problems.
- New orderings available :
- Modified Associative Path Ordering (Delor & Puel 93)
(implemented by Ralf
- Orderings by polynomial interpretations (implemented by Xavier
- 'Undo' in interactive ordering (implemented by Hubert Comon).
- Binary executables, compiled with the native code compiler of
Objective CAML (automatic translation thanks to Emmanuel Engel),
available by ftp for several architectures :
- Sparc under Solaris
- Sparc under SunOS 4.1
- Bugs corrected :
- A conflict in computation of AG normalising pairs in presence
of several AG theories (many thanks to Juergen Stuber who reported
- A bug in computation of transitive closure of precedences (many
thanks to Evelyne Contejean).
- A bug in computation of critical pairs of a rule with itself
at the top (many thanks to Fer-Jan de Vries).
Last modification of this page: september 10, 1997
Back to CiME