Associative-commutative unification
Unification in equational theories, that is, solving equations in varieties, is of special relevance to automated deduction. Major results in term rewriting systems, as by \textit{G. E. Peterson} and \textit{M. E. Stickel} [J. Assoc. Comput. Mach. 28, 233-264 (1981; Zbl 0479.68092)], depend on unification in presence of associative-commutative functions. \textit{M. E. Stickel} [ibid. 28, 423-434 (1981; Zbl 0462.68075)] gave an associative-commutative unification algorithm, but its termination in the general case was still questioned. The first part of this paper is an introduction to unification theory, the second part concerns the solving of homogeneous linear diophantine equations, and the third contains a proof of termination and correctness of the associative-commutative unification algorithm for the general case.
- A Machine-Oriented Logic Based on the Resolution Principle
- A Unification Algorithm for Associative-Commutative Functions
- An algorithm to generate the basis of solutions to homogeneous linear Diophantine equations
- An Efficient Unification Algorithm
- Complete Sets of Reductions for Some Equational Theories
- Complete sets of unifiers and matchers in equational theories
- Hilbert's Tenth Problem is Unsolvable
- scientific article; zbMATH DE number 3885353 (Why is no real title available?)
- scientific article; zbMATH DE number 3921983 (Why is no real title available?)
- scientific article; zbMATH DE number 3930337 (Why is no real title available?)
- scientific article; zbMATH DE number 3945372 (Why is no real title available?)
- scientific article; zbMATH DE number 4049025 (Why is no real title available?)
- scientific article; zbMATH DE number 4049130 (Why is no real title available?)
- scientific article; zbMATH DE number 3590511 (Why is no real title available?)
- scientific article; zbMATH DE number 3413831 (Why is no real title available?)
- On the sequential nature of unification
- Unification in abelian semigroups
- An algebraic approach to unification under associativity and commutativity
- Efficient solution of linear diophantine equations
- AC-unification race: The system solving approach, implementation and benchmarks
- A general refutational completeness result for an inference procedure based on associative-commutative unification
- A new method for undecidability proofs of first order theories
- Adventures in associative-commutative unification
- Competing for the \(AC\)-unification race
- A formally verified solver for homogeneous linear Diophantine equations
- Unification in permutative equational theories is undecidable
- Unification algorithms cannot be combined in polynomial time.
- A formalisation of nominal C-matching through unification with protected variables
- A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
- On the parameterized complexity of associative and commutative unification
- scientific article; zbMATH DE number 3866609 (Why is no real title available?)
- scientific article; zbMATH DE number 3871322 (Why is no real title available?)
- scientific article; zbMATH DE number 4203772 (Why is no real title available?)
- scientific article; zbMATH DE number 3930337 (Why is no real title available?)
- scientific article; zbMATH DE number 4043300 (Why is no real title available?)
- scientific article; zbMATH DE number 4074540 (Why is no real title available?)
- On the unification problem for Cartesian closed categories
- Unification algorithms cannot be combined in polynomial time
- Formalising nominal C-unification generalised with protected variables
- Open problems in rewriting
- AC-complete unification and its application to theorem proving
- “Syntactic” AC-unification
- Building Theorem Provers
- On pot, pans and pudding or how to discover generalised critical pairs
- On nominal syntax and permutation fixed points
- Unification in Boolean rings and Abelian groups
- Solving word equations
- When privacy fails, a formula describes an attack: a complete and compositional verification method for the applied \(\pi\)-calculus
- Nominal AC-matching
- Associative unification and symbolic reasoning modulo associativity in Maude
- Complexity of unification problems with associative-commutative operators
- Certified first-order AC-unification and applications.
- On the parameterized complexity of associative and commutative unification
- Automating the derivation of unification algorithms. A case study in deductive program synthesis
- Permutative rewriting and unification
This page was built for publication: Associative-commutative unification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1099648)
