A Coq Formalization of Unification Modulo Exclusive-Or

Yichi Xu, Daniel J. Dougherty, Rose Bohrer

Equational Unification is a critical problem in many areas such as automated theorem proving and security protocol analysis. In this paper, we focus on XOR-Unification, that is, un…