On equational theories, unification, and (un)decidability
type: Item
instance of: scholarly article
title: On equational theories, unification, and (un)decidability
zbMATH Open document ID: 0684.03004
DOI: 10.1016/S0747-7171(89)80021-5
author: Hans-Jürgen Bürckert
author: Alexander Herold
author: Manfred Schmidt-Schauß
published in: Journal of Symbolic Computation
publication date: 1989-01-01T00:00:00Z
review text: We investigate the following classes of equational theories which are important in unification theory: permutative, finite, Noetherian, almost collapse free, collapse free, regular, and \(\Omega\)-free theories. We show some relationships between the particular classes and their connections to the unification hierarchy. Especially, we study conditions under which minimal and complete sets of unifiers always exist. We have some undecidability results for the membership problem of equational theories to these classes (the `class problem'): simplicity, almost collapse freeness, and \(\Omega\)-freeness are undecidable properties. Finiteness is known to be also undecidable, and the other investigated properties, permutativity, regularity, collapse freeness, are known to be trivially decidable. We give an equational theory where every single equation has a minimal set of unifiers, however, for some systems of equations no minimal set of unifiers exists. This example suggests that the definition of a unification problem has to be modified and that the definitions of the unification types have to be adapted accordingly.
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03C05
Mathematics Subject Classification ID: 03B25
zbMATH DE Number: 4120147
zbMATH Keywords: solving equations
zbMATH Keywords: decidability
zbMATH Keywords: equational theories
zbMATH Keywords: unification
zbMATH Keywords: undecidability
MaRDI profile type: Publication
cites work: The theory of idempotent semigroups is of unification type zero
cites work: Q5762080
cites work: On unification: Equational theories are not bounded
cites work: The word problem
cites work: Unification in Boolean rings and Abelian groups
cites work: Q5663380
cites work: History and basic features of the critical-pair/completion procedure
cites work: Q3786017
cites work: Q3779785
cites work: Q3934450
cites work: Embedding Boolean expressions into logic programming
cites work: Q5679729
cites work: Termination of rewriting
cites work: Properties of substitutions and unifications
cites work: Q3335752
cites work: Complete sets of unifiers and matchers in equational theories
cites work: Initial Algebra Semantics and Continuous Algebras
cites work: Q4200260
cites work: Q3786019
cites work: Q3835440
cites work: Q3862379
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Q3883561
cites work: Q3338225
cites work: Q5581665
cites work: New decision algorithms for finitely presented commutative semigroups
cites work: Q5804999
cites work: The decision problem for equational bases of algebras
cites work: An Efficient Unification Algorithm
cites work: Q3786022
cites work: Complexity of certain decision problems about congruential languages
cites work: On the algorithmic insolvability of the word problem in group theory
cites work: Linear unification
cites work: Q5678447
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Unification under associativity and idempotence is of type nullary
cites work: Unification in permutative equational theories is undecidable
cites work: Q3811748
cites work: Q3338215
cites work: Q3484383
cites work: Q3313256
cites work: Q3853703
cites work: Q3785922
cites work: Q3030272
cites work: Unification problems with one-sided distributivity
cites work: The Concept of Demodulation in Theorem Proving
cites work: Q3716322
cites work: Unification in combinations of collapse-free regular theories
description: scientific article; zbMATH DE number 4120147