The undecidability of the unification and matching problem for canonical theories
type: Item
instance of: scholarly article
title: The undecidability of the unification and matching problem for canonical theories
zbMATH Open document ID: 0595.68031
DOI: 10.1007/BF00264362
author: Stephan Heilbrunner
author: Steffen Hölldobler
published in: Acta Informatica
publication date: 1987-01-01T00:00:00Z
review text: The problem whether there exists a unifying substitution for two terms is considered in the class of theories which can be embedded into canonical term rewriting systems. The problem is shown to be undecidable, even if we restrict the substitutions to matching ones. This implies that the class of admissible canonical theories is a proper subset of the class of canonical theories.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 3958719
zbMATH Keywords: term rewriting systems
zbMATH Keywords: admissible canonical theories
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00264362
OpenAlex ID: W2008100839
Recommended article: A note on a canonical theory with undecidable unification and matching problem
Recommended article: The undecidability of the DA-unification problem
Recommended article: The undecidability of the semi-unification problem
Recommended article: On equational theories, unification, and (un)decidability
Recommended article: Unification in permutative equational theories is undecidable
Recommended article: On unification: Equational theories are not bounded
Recommended article: On the undecidability of second-order unification
Recommended article: Unification problem in equational theories
Recommended article: The undecidability of simultaneous rigid E-unification
Recommended article: The undecidability of the second order predicate unification problem
description: scientific article; zbMATH DE number 3958719