Complexity of unification problems with associative-commutative operators

DOI10.1007/BF00245463zbMath0781.68076MaRDI QIDQ688565

Deepak Kapur, Paliath Narendran

Publication date: 20 December 1993

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

zbMATH Keywords

idempotentmatchingunificationNP-completeunitword equationsidentityequational theoriesassociativecommutativeset matching

Mathematics Subject Classification ID

Related Items (24)

Generating languages by a derivation procedure for elementary formal systems ⋮ More problems in rewriting ⋮ An algorithm for distributive unification ⋮ An efficient labelled nested multiset unification algorithm ⋮ The complexity of counting problems in equational matching ⋮ \(E\)-unification with constants vs. general \(E\)-unification ⋮ Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification ⋮ Extensions of unification modulo ACUI ⋮ On the unification problem for Cartesian closed categories ⋮ What Is Essential Unification? ⋮ Combination techniques and decision problems for disunification ⋮ Unification and matching modulo nilpotence ⋮ Unification theory ⋮ Combination techniques and decision problems for disunification ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ On the parameterized complexity of associative and commutative unification ⋮ AC-superposition with constraints: No AC-unifiers needed ⋮ Approximate Unification in the Description Logic $$\mathcal {FL}_0$$ ⋮ Type dependencies for logic programs using ACI-unification ⋮ A formalisation of nominal C-matching through unification with protected variables ⋮ Complexity of nilpotent unification and matching problems. ⋮ Unification algorithms cannot be combined in polynomial time. ⋮ Formalising nominal C-unification generalised with protected variables ⋮ Cancellative Abelian monoids and related structures in refutational theorem proving. I

Cites Work

• Unification in varieties of idempotent semigroups
• Complexity of matching problems
• Unification problems with one-sided distributivity
• Unification theory
• Linear unification
• Matching, unification and complexity
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• A Unification Algorithm for Associative-Commutative Functions
• Complete Sets of Reductions for Some Equational Theories
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Complexity of unification problems with associative-commutative operators