In this paper, we consider the unification problem over theories that are extensions of ACI or ACUI, obtained by adding finitely many homomorphism symbols, or a symbol ‘∗’ that distributes over the ACUI-symbol denoted ‘+’. We first show that when we adjoin a set of commuting homomorphisms to ACUI, unification is undecidable. We then consider the ACUIDl-unification problem, i.e., unification modulo ACUI plus left-distributivity of a given ‘∗’ w.r.t. ‘+’, and prove its NEXPTIME-decidability. When we assume the symbol ‘∗’ to be 2-sided distributive w.r.t. ‘+’, we get the theory ACUID, for which the unification problem remains decidable. But when equations of associativitycommutativity, or just of associativity, on ‘∗’ are added on to ACUID, the unification problem becomes undecidable.
CITATION STYLE
Anantharaman, S., Narendran, P., & Rusinowitch, M. (2003). Unification modulo ACUI plus homomorphisms/distributivity. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2741, pp. 442–457). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_38
Mendeley helps you to discover research relevant for your work.