Termination Checker and Knuth-Bendix Completion Tools for Maude Equational Specifications

Francisco Durán

This document explains the design and use of a termination checker tool and of a Knuth-Bendix completion tool. The termination checker tool checks whether an equational specification terminates, and the Knuth-Bendix completion tool tries to complete an equational specification. These tools can be used to prove the termination or to complete order-sorted equational specifications in Maude. The tools have been written entirely in Maude and are in fact executable specifications in rewriting logic of the formal inference system that they implement. The fact that rewriting logic is reflective, and that Maude efficiently supports reflective rewriting logic computations is systematically exploited in the design of the tools.

(BibTeX entry)    (gzip'ed Postscript)   

back   home   Formal Methods and Declarative Languages Laboratory   Computer Science Laboratory, SRI International