TY - GEN
T1 - Asymmetric unification
T2 - 24th International Conference on Automated Deduction, CADE 2013
AU - Erbatur, Serdar
AU - Escobar, Santiago
AU - Kapur, Deepak
AU - Liu, Zhiqiang
AU - Lynch, Christopher A.
AU - Meadows, Catherine
AU - Meseguer, José
AU - Narendran, Paliath
AU - Santiago, Sonia
AU - Sasse, Ralf
N1 - Funding Information:
S. Escobar and S. Santiago were partially supported by EU (FEDER) and the Spanish MEC/MICINN under grant TIN 2010-21062-C02-02, and by Generalitat Valenciana PROMETEO2011/052. The following authors were partially supported by NSF: S. Escobar, J. Meseguer, and R. Sasse under CNS 09-04749 and CCF 09-05584; D. Kapur under CNS 09-05222; C. Lynch, Z. Liu, and C. Meadows under CNS 09-05378, and P. Narendran and S. Erbatur under CNS 09-05286. Part of the S. Erbatur’s work was supported while with the Department of Computer Science, University at Albany, and part of R. Sasse’s work was supported while with the Department of Computer Science, University of Illinois at Urbana-Champaign. Portions of this paper appeared in an abstract in the informal proceedings of UNIF’11.
PY - 2013
Y1 - 2013
N2 - We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition of an equational theory into (R,E) where R is confluent, terminating, and coherent modulo E, and (ii) on reducing unification problems to a set of problems s =? t under the constraint that t remains R/E-irreducible. We call this method asymmetric unification. We first present a general-purpose generic asymmetric unification algorithm. and then outline an approach for converting special-purpose conventional unification algorithms to asymmetric ones, demonstrating it for exclusive-or with uninterpreted function symbols. We demonstrate how asymmetric unification can improve performanceby running the algorithm on a set of benchmark problems. We also give results on the complexity and decidability of asymmetric unification.
AB - We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition of an equational theory into (R,E) where R is confluent, terminating, and coherent modulo E, and (ii) on reducing unification problems to a set of problems s =? t under the constraint that t remains R/E-irreducible. We call this method asymmetric unification. We first present a general-purpose generic asymmetric unification algorithm. and then outline an approach for converting special-purpose conventional unification algorithms to asymmetric ones, demonstrating it for exclusive-or with uninterpreted function symbols. We demonstrate how asymmetric unification can improve performanceby running the algorithm on a set of benchmark problems. We also give results on the complexity and decidability of asymmetric unification.
UR - http://www.scopus.com/inward/record.url?scp=84879987551&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84879987551&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-38574-2_16
DO - 10.1007/978-3-642-38574-2_16
M3 - Conference contribution
AN - SCOPUS:84879987551
SN - 9783642385735
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 231
EP - 248
BT - CADE 2013 - 24th International Conference on Automated Deduction, Proceedings
Y2 - 9 June 2013 through 14 June 2013
ER -