A Unification Algorithm for Associative-Commutative Functions
From MaRDI portal
Publication:3912070
DOI10.1145/322261.322262zbMath0462.68075WikidataQ56609900 ScholiaQ56609900MaRDI QIDQ3912070
Publication date: 1981
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/322261.322262
Related Items
On the unification problem for Cartesian closed categories, A Folding Algorithm for Eliminating Existential Variables from Constraint Logic Programs, On the complexity of recognizing the Hilbert basis of a linear Diophantine system, On the complexity of deduction modulo leaf permutative equations, Unification in commutative theories, Unification in Boolean rings and Abelian groups, Unification in a combination of arbitrary disjoint equational theories, Towards a foundation of completion procedures as semidecision procedures, Complexity of unification problems with associative-commutative operators, Refutational theorem proving using term-rewriting systems, Permutative rewriting and unification, A superposition oriented theorem prover, On unification: Equational theories are not bounded, Complexity of matching problems, Associative-commutative unification, Unification in combinations of collapse-free regular theories, An algebraic approach to unification under associativity and commutativity, Embedding Boolean expressions into logic programming, History and basic features of the critical-pair/completion procedure, Only prime superpositions need be considered in the Knuth-Bendix completion procedure, Unification in commutative idempotent monoids, Efficient solution of linear diophantine equations, Combination of constraint solvers for free and quasi-free structures, Completion for unification, AC-unification race: The system solving approach, implementation and benchmarks, A new method for undecidability proofs of first order theories, Completion for rewriting modulo a congruence, Adventures in associative-commutative unification, Unification problem in equational theories, Competing for the \(AC\)-unification race, Unification in partially commutative semigroups, Automated deduction with associative-commutative operators, Avoiding slack variables in the solving of linear diophantine equations and inequations, Ramification and causality, Type dependencies for logic programs using ACI-unification, Complete sets of unifiers and matchers in equational theories, Unification in permutative equational theories is undecidable, Unification algorithms cannot be combined in polynomial time., Alternating two-way AC-tree automata, Linear groupoids and the associated wreath products., Abstraction and resolution modulo AC: How to verify Diffie--Hellman-like protocols automatically, Unnecessary inferences in associative-commutative completion procedures
