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

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.
 
 
 

Maude Specifications and Samples

• Termination Checker and Knuth-Bendix Completion Tools for Maude Equational Specifications (kbc.tar)

Instructions: Load full-maude.maude and then kbc.maude. Then start the loop (loop init .). The tool is now ready for entering the examples below.
 
• Examples:

Group Theory I (ex-kbc-group-I.fm)

Group Theory II (ex-kbc-group-II.fm)

The Inverse Property (ex-kbc-inverse.fm)

Uniqueness of the Identity and Inverse Functions (ex-kbc-group-III.fm)

Central Groupoids (ex-kbc-groupoids.fm)

Central Groupoids II (ex-kbc-groupoids-II.fm)

Defining New Orders (ex-kbc-group-IV.fm)

The Use of the Commutative Attribute (ex-kbc-group-V.fm)

Completion of a Specification of the Integer Numbers (ex-kbc-integers-I.fm)

Conditional Specifications: A Second Specification of the Integer Numbers (ex-kbc-integers-II.fm)

• Termination Checker and Knuth-Bendix Completion Tools for Maude Equational Specifications. By Francisco Durán. Manuscript. Universidad de Málaga. July 2000.