A Coq Formalization of Unification Modulo Exclusive-Or
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917920943112192 |
|---|---|
| author | Xu, Yichi Dougherty, Daniel J. Bohrer, Rose |
| author_facet | Xu, Yichi Dougherty, Daniel J. Bohrer, Rose |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2502_09225 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Coq Formalization of Unification Modulo Exclusive-Or Xu, Yichi Dougherty, Daniel J. Bohrer, Rose Logic in Computer Science Cryptography and Security 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. |
| title | A Coq Formalization of Unification Modulo Exclusive-Or |
| topic | Logic in Computer Science Cryptography and Security |
| url | https://arxiv.org/abs/2502.09225 |