@inproceedings{LLT06,
title = { {ACUNh}: Unification and Disunification Using Automata Theory },
author = {Lafourcade, Pascal and Lugiez, Denis and Treinen, Ralf},
month = {aug},
year = {2006},
booktitle = {{P}roceedings of the 20th {I}nternational {W}orkshop on {U}nification ({UNIF}'06)},
address = {Seattle, Washington, USA},
pages = {6-20},
team = {other},
abstract = {We show several results about unification problems in the equational theory~ACUNh consisting of the theory of exclusive or with one homomorphism. These results are shown using only techniques of automata and combinations of unification problems. We~show how to construct a most-general unifier for ACUNh-unification problems with constants using automata. We also prove that the first-order theory of ground terms modulo~ACUNh is decidable if the signature does not contain free non-constant function symbols, and that the existential fragment is decidable in the general case. Furthermore, we show a technical result about the set of most-general unifiers obtained for general unification problems.},
}
