Unification modulo ACUI plus Distributivity Axioms
type: Dataset
description: 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)ID_l; we show that AC(U)ID_l-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)ID_l 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.
issued: 2026-05-15T08:30:59.977845
language: en
modified: 2026-05-15T08:30:59.977851
contact point: Organization
  fn: CCSD
keyword: complexity
keyword: counter-machines
keyword: decidability
keyword: equational-unification
keyword: infoeu-reposemanticsarticle
keyword: infoinfo-clcomputer-science-cscomputation-and-language-cscl
keyword: journal-articles
keyword: post-correspondence-problem
keyword: rewriting
keyword: set-constraints
landing page: 0168-7433

Unification modulo ACUI plus Distributivity Axioms
type: Distribution
format: HTML
issued: 2026-05-15T08:31:00.008830
modified: 2026-05-15T08:30:59.958382
access URL: https://hal.science/hal-00077499

test_moissonnage_selune
type: Agent