Declarative Debugging of Missing Answers for Maude

Authors Adrian Riesco, Alberto Verdejo, Narciso Marti-Oliet

Thumbnail PDF


  • Filesize: 206 kB
  • 18 pages

Document Identifiers

Author Details

Adrian Riesco
Alberto Verdejo
Narciso Marti-Oliet

Cite AsGet BibTex

Adrian Riesco, Alberto Verdejo, and Narciso Marti-Oliet. Declarative Debugging of Missing Answers for Maude. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 277-294, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Declarative debugging is a semi-automatic technique that starts from an incorrect computation and locates a program fragment responsible for the error by building a tree representing this computation and guiding the user through it to find the error. Membership equational logic (MEL) is an equational logic that in addition to equations allows the statement of membership axioms characterizing the elements of a sort. Rewriting logic is a logic of change that extends MEL by adding rewrite rules, that correspond to transitions between states and can be nondeterministic. In this paper we propose a calculus that allows to infer normal forms and least sorts with the equational part, and sets of reachable terms through rules. We use an abbreviation of the proof trees computed with this calculus to build appropriate debugging trees for missing answers (results that are erroneous because they are incomplete), whose adequacy for debugging is proved. Using these trees we have implemented a declarative debugger for Maude, a high-performance system based on rewriting logic, whose use is illustrated with an example.
  • Declarative debugging
  • Maude
  • Missing answers
  • Rewriting


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail