A Coq Formalization of Unification Modulo Exclusive-Or
Logic in Computer Science
2025-02-14 v1 Cryptography and Security
Abstract
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, unification modulo the theory of exclusive-or. This theory contains an operator with the properties Associativity, Commutativity, Nilpotency, and the presence of an identity. In the proof assistant Coq, we implement an algorithm that solves XOR unification problems, whose design was inspired by Liu and Lynch, and prove it sound, complete, and terminating. Using Coq's code extraction capability we obtain an implementation in the programming language OCaml.
Keywords
Cite
@article{arxiv.2502.09225,
title = {A Coq Formalization of Unification Modulo Exclusive-Or},
author = {Yichi Xu and Daniel J. Dougherty and Rose Bohrer},
journal= {arXiv preprint arXiv:2502.09225},
year = {2025}
}
Comments
In Proceedings ICLP 2024, arXiv:2502.08453