On unification: Equational theories are not bounded
type: Item
instance of: scholarly article
title: On unification: Equational theories are not bounded
zbMATH Open document ID: 0629.68037
DOI: 10.1016/S0747-7171(86)80001-3
author: Ronald V. Book
author: Jörg H. Siekmann
published in: Journal of Symbolic Computation
publication date: 1986-01-01T00:00:00Z
review text: We are interested in first-order unification problems and, more specifically, in the hierarchy of equational theories based on the cardinality of the set of most general unifiers. The following result is established in this paper: if T is a suitable first-order equational theory that is not unitary, then T is not bounded; that is, there is no integer \(n>1\) such that for every unification problem \(<s=t>_ T\), the cardinality of the set of most general unifiers for \(<s=t>_ T\) is at most n. Hence, the class of (non-unitary) finitary theories cannot be decomposed into a hierarchy obtained by uniformly bounding the cardinalities of the sets of most general unifiers.
Mathematics Subject Classification ID: 68W30
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4024778
zbMATH Keywords: first-order unification
zbMATH Keywords: equational theories
MaRDI profile type: Publication
cites work: Q3335752
cites work: Q5572358
cites work: Q5678447
cites work: Q3338215
cites work: A Unification Algorithm for Associative-Commutative Functions
full work available at URL: s0747-7171(86)80001-3
OpenAlex ID: W1988552011
description: scientific article; zbMATH DE number 4024778