| Overview |
The tools discussed in these pages, namely the Church-Rosser, termination, and coherence checkers and the Knuth-Bendix and Coherence completion tools can be easily interoperated. As illustrated in, for example, the documentation of the Church-Rosser checker and in Duran's thesis, different tools can be interoperated just by creating an environment which behaves as each of the environments of each of the tools, that is, by creating an appropriate object inheriting of all of them.
Instructions: Load full-maude.maude and then tools.maude.
Then start the loop (loop init .). The tool is now ready for entering the
examples given for each of the tools.
| [Maude Home Page] |