On equational theories, unification, and (un)decidability

DOI10.1016/S0747-7171(89)80021-5zbMath0684.03004MaRDI QIDQ1825184

Hans-Jürgen Bürckert, Alexander Herold, Manfred Schmidt-Schauss

Publication date: 1989

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

zbMATH Keywords

undecidabilitydecidabilityunificationsolving equationsequational theories

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05)

Related Items (8)

Algebraic and logical aspects of unification ⋮ Unification theory ⋮ AC-unification race: The system solving approach, implementation and benchmarks ⋮ A new method for undecidability proofs of first order theories ⋮ Essential unifiers ⋮ Unnamed Item ⋮ A partial evaluation framework for order-sorted equational programs modulo axioms ⋮ Order-sorted Homeomorphic Embedding Modulo Combinations of Associativity and/or Commutativity Axioms*

Cites Work

• Unification under associativity and idempotence is of type nullary
• The theory of idempotent semigroups is of unification type zero
• Unification in Boolean rings and Abelian groups
• Properties of substitutions and unifications
• Complexity of certain decision problems about congruential languages
• On unification: Equational theories are not bounded
• Termination of rewriting
• Unification problems with one-sided distributivity
• Unification in combinations of collapse-free regular theories
• Embedding Boolean expressions into logic programming
• History and basic features of the critical-pair/completion procedure
• New decision algorithms for finitely presented commutative semigroups
• Linear unification
• Complete sets of unifiers and matchers in equational theories
• Unification in permutative equational theories is undecidable
• On the algorithmic insolvability of the word problem in group theory
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• An Efficient Unification Algorithm
• Initial Algebra Semantics and Continuous Algebras
• The decision problem for equational bases of algebras
• A Machine-Oriented Logic Based on the Resolution Principle
• The Concept of Demodulation in Theorem Proving
• The word problem
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On equational theories, unification, and (un)decidability