HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

Unification Modulo ACUI Plus Distributivity Axioms

Siva Anantharaman 1 Paliath Narendran Michaël Rusinowitch 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 `*' that distributes over the AC(U)I-symbol `+'. 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 `*' is assumed $2$-sided distributive over `+', 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, e.g. in the analysis of programs modeled in terms of process algebras. Our results, for the two theories considered, are obtained via two entirely different lines of reasoning. It is a consequence of our methods of proof, that modulo the theory which adds on to AC(U)ID the assumption that `*' is associative-commutative -- or just associative --, unification is undecidable.
Document type :
Journal articles
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 10:13:14 AM
Last modification on : Friday, January 21, 2022 - 3:08:37 AM

Links full text



Siva Anantharaman, Paliath Narendran, Michaël Rusinowitch. Unification Modulo ACUI Plus Distributivity Axioms. Journal of Automated Reasoning, Springer Verlag, 2004, 33, pp.1-28. ⟨10.1007/s10817-004-2279-7⟩. ⟨inria-00099990⟩



Record views