Coherence Checker and Completion Tools for Maude Specifications

This document explains the design and use of a coherence checker tool and of a coherence completion tool. The coherence checker tool checks whether a rewrite logic specification is coherent, and the coherence completion tool tries to complete a rewrite logic specification in order to make it coherent. These tools can be used to prove the coherence property or to coherence complete order-sorted rewrite 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

• Coherence Checker and Completion Tools for Maude Specifications (coherence.tar)

Instructions: Load full-maude.maude and then coh-check.maude (for the checker) or coh-compl.maude (for the completion tool). Then start the loop (loop init .). The tool is now ready for entering the examples below.
 
• Examples:

Rewriting Modulo Commutativity with an Identity Equation (ex-coh-identity.fm)

Sequent Calculus for Propositional Logic (ex-coh-prop-calc.fm)

A Nondeterministic Choice Operator (ex-coh-choice.fm)

• Coherence Checker and Completion Tools for Maude Specifications. By Francisco Durán. Manuscript. Universidad de Málaga. July 2000.