View Related Documents

Abstract

E-unification problems are central in automated deduction. In this work, we consider unification modulo theories that extend the well-known ACI or ACUI by adding a binary symbol ldquo*rdquo that distributes over the AC(U)I-symbol ldquo+.rdquo If this distributivity is one-sided (say, to the left), we get the theory denoted AC(U)IDl; we show that AC(U)IDl-unification is DEXPTIME-complete. If ldquo*rdquo is assumed two-sided distributive over ldquo+,rdquo we get the theory denoted AC(U)ID; we show unification modulo AC(U)ID to be NEXPTIME-decidable and DEXPTIME-hard. Both AC(U)IDl and AC(U)ID seem to be of practical interest, for example, in the analysis of programs modeled in terms of process algebras. Our results, for the two theories considered, are obtained through two entirely different lines of reasoning. A consequence of our methods of proof is that, modulo the theory that adds to AC(U)ID the assumption that ldquo*rdquo is associative-commutative, or just associative, unification is undecidable.

Keywords  rewriting - equational unification - counter machines - Post correspondence problem - set constraints - decidability - complexity

Fulltext Preview

Image of the first page of the fulltext document