Equational Unification is a critical problem in many areas such as automated theorem proving and security protocol analysis. In this paper, we focus on XORUnification, that is, unification modulo the theory of exclusive-or. This theory contains a function with the properties Associativity, Commutativity, Nilpotency, and the presence of an identity. In the proof assistant Coq, we implement an algorithm inspired by Liu and Lynch’s inference rules and prove it sound, complete, and terminating. Using Coq’s code extraction capability one obtains an implementation in the programming language Ocaml.

Creator

• Xu, Yichi

Contributors

• Dougherty, Daniel J.

Degree

• MS

Publisher

• Worcester Polytechnic Institute

Identifier

• etd-105116

Advisor

• Dougherty, Daniel J.

Defense date

• 2023-04-20

Year

• 2023

Date created

• 2023-04-26

Resource type

• Thesis

Source

• etd-105116

Rights statement

• In Copyright

Last modified

• 2023-06-06