The CiME 1.13 distribution

• Documentation
• Binaries for some architectures:
  • for SPARC stations running Solaris (at least version 2.4)
  • for SPARC stations running Sun OS (at least version 4.1)
  • for HP workstations running HP-UX (at least version 10.01)
  • for PC running Linux (at least version 1.2)
• Sources (needed only if you work on another architecture than the ones above)
• Utilities: an emacs mode, a LaTeX style file
• Examples, including the famous Chameleon's Quiz

What's New ?

• Unification : E-unification is now available for E=ACU,AG and BR. Both plain and AC-complete forms, as defined in (Boudet, Contejean & Marche 96) (implemented by Evelyne Contejean ).
• Completion :
  • Completion strategy completed changed, due to AC-complete unification.
  • 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 Treinen).
  • Orderings by polynomial interpretations (implemented by Xavier Urbain).
  • '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
  • Linux
• Bugs corrected :
  • A conflict in computation of AG normalising pairs in presence of several AG theories (many thanks to Juergen Stuber who reported that bug).
  • 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).