A sufficient completeness reasoning tool for partial specifications

Joe Hendrix, Manuel Clavel, José Meseguer

Research output: Contribution to journalConference articlepeer-review


We present the Maude sufficient completeness tool, which explicitly supports sufficient completeness reasoning for partial conditional specifications having sorts and subsorts and with domains of functions defined by conditional memberships. Our tool consists of two main components: (i) a sufficient completeness analyzer that generates a set of proof obligations which if discharged, ensures sufficient completeness; and (ii) Maude's inductive theorem prover (ITP) that is used as a back-end to try to automatically discharge those proof obligations.

Original languageEnglish (US)
Pages (from-to)165-174
Number of pages10
JournalLecture Notes in Computer Science
StatePublished - 2005
Event16th International Conference on Term Rewriting and Applications, RTA 2005 - Nara, Japan
Duration: Apr 19 2005Apr 21 2005

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A sufficient completeness reasoning tool for partial specifications'. Together they form a unique fingerprint.

Cite this