Complete sets of unifiers and matchers in equational theories

DOI10.1016/0304-3975(86)90175-1zbMath0615.03002OpenAlexW2148193906WikidataQ56092426 ScholiaQ56092426MaRDI QIDQ1820760

François Fages, Gérard Huet

Publication date: 1986

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(86)90175-1

zbMATH Keywords

matchingunificationequational theories

Mathematics Subject Classification ID

Related Items (31)

Semi-unification of two terms in Abelian groups ⋮ Unification in varieties of idempotent semigroups ⋮ Characterizations of unification type zero ⋮ Rewriting, and equational unification: the higher-order cases ⋮ Decidability of confluence and termination of monadic term rewriting systems ⋮ A note on unification type zero ⋮ Associative-commutative unification ⋮ The undecidability of the D_A-unification problem ⋮ Inheritance hierarchies: Semantics and unifications ⋮ Unification properties of commutative theories: A categorical treatment ⋮ Implementation of Makanin's Algorithm ⋮ Complete equational unification based on an extension of the Knuth-Bendix completion procedure ⋮ The complexity of counting problems in equational matching ⋮ Anti-unification and the theory of semirings ⋮ The unification hierarchy is undecidable ⋮ What Is Essential Unification? ⋮ Unification algorithms cannot be combined in polynomial time ⋮ An improved general \(E\)-unification method ⋮ Solving word equations ⋮ Unification in commutative theories ⋮ Order-sorted unification ⋮ Unification in a combination of arbitrary disjoint equational theories ⋮ Matching - a special case of unification? ⋮ Variadic equational matching in associative and commutative theories ⋮ Solving word equations ⋮ Completion for rewriting modulo a congruence ⋮ Complete sets of transformations for general E-unification ⋮ Schematization of infinite sets of rewrite rules generated by divergent completion processes ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ On equational theories, unification, and (un)decidability ⋮ Unification algorithms cannot be combined in polynomial time.

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• New decision algorithms for finitely presented commutative semigroups
• The undecidability of the second-order unification problem
• Complexity of the unification algorithm for first-order expressions
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• Linear unification
• An algorithm to generate the basis of solutions to homogeneous linear Diophantine equations
• A Unification Algorithm for Associative-Commutative Functions
• An Efficient Unification Algorithm
• Complete Sets of Reductions for Some Equational Theories
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• The undecidability of the third order dyadic unification problem
• Hilbert's Tenth Problem is Unsolvable
• A Machine-Oriented Logic Based on the Resolution Principle
• The undecidability of unification in third order logic

This page was built for publication: Complete sets of unifiers and matchers in equational theories