Complete sets of unifiers and matchers in equational theories

DOI10.1016/0304-3975(86)90175-1zbMath0615.03002WikidataQ56092426 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

matching; unification; equational theories

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Related Items

Solving word equations, 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?, Unification in varieties of idempotent semigroups, A note on unification type zero, Associative-commutative unification, Inheritance hierarchies: Semantics and unifications, The unification hierarchy is undecidable, An improved general \(E\)-unification method, 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, Semi-unification of two terms in Abelian groups, Higher-order unification revisited: Complete sets of transformations, On equational theories, unification, and (un)decidability, Unification algorithms cannot be combined in polynomial time., The undecidability of the D_A-unification problem

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