Order-sorted equational unification revisited

Joe Hendrix, José Meseguer

Research output: Contribution to journalArticlepeer-review


This paper presents a rule-based algorithm for performing order-sorted E-unification using an unsorted E-unification decision procedure under assumptions about E that are commonly satisfied in practice. We have implemented this algorithm in Maude for use with the Maude-NRL protocol analyzer and have used CiME for unsorted E-unification for E any set of AC and ACU axioms. In many examples of interest, using order-sorted unification over unsorted unification is able to reduce the total number of unifiers considered, and dramatically improve the performance of the Maude-NRL tool.

Original languageEnglish (US)
Pages (from-to)37-50
Number of pages14
JournalElectronic Notes in Theoretical Computer Science
StatePublished - Dec 20 2012


  • Order-sorted unification
  • rule-based programming

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Order-sorted equational unification revisited'. Together they form a unique fingerprint.

Cite this