Unification in permutative equational theories is undecidable

DOI10.1016/S0747-7171(89)80037-9zbMath0684.03019MaRDI QIDQ1825190

Manfred Schmidt-Schauss

Publication date: 1989

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

Turing machineconfluent term-rewriting systempermutative equational theoriesunifiability of terms

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Abstract data types; algebraic specification (68Q65) Equational classes, universal algebra in model theory (03C05) Turing machines and related notions (03D10)

Related Items

Model Checking Security Protocols ⋮ Decidability of confluence and termination of monadic term rewriting systems ⋮ Unnamed Item ⋮ Permutative rewriting and unification ⋮ It is undecidable whether the Knuth-Bendix completion procedure generates a crossed pair ⋮ An Oxford survey of order sorted algebra ⋮ Computing knowledge in equational extensions of subterm convergent theories ⋮ On equational theories, unification, and (un)decidability

Cites Work

• Unification in abelian semigroups
• Associative-commutative unification
• An algebraic approach to unification under associativity and commutativity
• Unification theory
• New decision algorithms for finitely presented commutative semigroups
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Unification Algorithm for Associative-Commutative Functions
• A Machine-Oriented Logic Based on the Resolution Principle
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item