The unification hierarchy is undecidable

DOI10.1007/BF00249020zbMath0744.03016OpenAlexW2074681477MaRDI QIDQ1181721

Werner Nutt

Publication date: 27 June 1992

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

Full work available at URL: https://doi.org/10.1007/bf00249020

zbMATH Keywords

matchingequational theoriesunification hierarchy

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (2)

Combination problems for commutative/monoidal theories or how algebra can help in equational unification ⋮ Unification in varieties of completely regular semigroups

Cites Work

• Unification under associativity and idempotence is of type nullary
• The theory of idempotent semigroups is of unification type zero
• Unification in a combination of arbitrary disjoint equational theories
• On unification: Equational theories are not bounded
• Unification theory
• Complete sets of unifiers and matchers in equational theories
• Unsolvable problems for equational theories
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The unification hierarchy is undecidable