ORME a toolbox of functions for rewriting, rewriting and AC-rewiting together with a procedure of AC-completion. Most of ORME is written in CAML (V3.1). It is developed by Prof. Pierre Lescanne from INRIA-Lorraine, BP 239, F-54506 Vandoeuvre-les-Nancy Cedex, France. ORME is available on SUN by anonymous ftp at ftp.loria.fr:/pub/loria/eureca/ORME
For a detailed introduction to ORME read:
P. Lescanne, Completion Procedures as Transition Rules + Control, Colloquium Current Concept In Programming Languages, TAPSOFT, Barcelona (Spain) Lecture Notes in Computer Science 351, Springer Verlag (1989), pp 28-41.
P. Lescanne, Implementation of Completion by Transition Rules + Control: ORME, second international conference Algebraic and Logic Programming, Nancy, Lecture Notes in Computer Science 463, Springer Verlag (1990), pp 262-269.
E. Domenjoud, Outils pour la deduction automatique dans les theories associatives-commutatives, these U. Nancy 1, september 1991.