Abstract
We consider the unification problem for the equational theory AC(U)ID obtained by adjoining a binary V which is distributive over an associative-commutative idempotent operator '+', possibly admitting a unit element U. We formulate the problem as a particular class of set constraints, and propose a method for solving it by using the dag automata introduced by W. Charatonik, that we enrich with labels for our purposes. AC(U)ID-unification is thus shown to be in NEXPTIME. © Springer-Verlag Berlin Heidelberg 2003.
Author supplied keywords
Cite
CITATION STYLE
Anantharaman, S., Narendran, P., & Rusinowitch, M. (2003). ACID-unification is NEXPTIME-decidable. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2747, 169–178. https://doi.org/10.1007/978-3-540-45138-9_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
