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.},


Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4006242