by Francisco Durán
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.
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.
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)