TY - JOUR
T1 - Order-sorted equational unification revisited
AU - Hendrix, Joe
AU - Meseguer, José
N1 - Funding Information:
1 The research has been supported in part by ONR grant N00014-02-1-0715 and NSF grant CNS-07-16638. 2 Email: [email protected] 3 Email: [email protected]
PY - 2012/12/20
Y1 - 2012/12/20
N2 - 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.
AB - 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.
KW - Order-sorted unification
KW - rule-based programming
UR - http://www.scopus.com/inward/record.url?scp=84871258061&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84871258061&partnerID=8YFLogxK
U2 - 10.1016/j.entcs.2012.11.010
DO - 10.1016/j.entcs.2012.11.010
M3 - Article
AN - SCOPUS:84871258061
SN - 1571-0661
VL - 290
SP - 37
EP - 50
JO - Electronic Notes in Theoretical Computer Science
JF - Electronic Notes in Theoretical Computer Science
ER -