Associative-commutative unification
type: Item
instance of: scholarly article
title: Associative-commutative unification
zbMATH Open document ID: 0638.68103
DOI: 10.1016/S0747-7171(87)80004-4
author: François Fages
published in: Journal of Symbolic Computation
publication date: 1987-01-01T00:00:00Z
review text: Unification in equational theories, that is, solving equations in varieties, is of special relevance to automated deduction. Major results in term rewriting systems, as by \textit{G. E. Peterson} and \textit{M. E. Stickel} [J. Assoc. Comput. Mach. 28, 233-264 (1981; Zbl 0479.68092)], depend on unification in presence of associative-commutative functions. \textit{M. E. Stickel} [ibid. 28, 423-434 (1981; Zbl 0462.68075)] gave an associative-commutative unification algorithm, but its termination in the general case was still questioned. The first part of this paper is an introduction to unification theory, the second part concerns the solving of homogeneous linear diophantine equations, and the third contains a proof of termination and correctness of the associative-commutative unification algorithm for the general case.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 08B05
Mathematics Subject Classification ID: 11D04
zbMATH DE Number: 4041329
zbMATH Keywords: Unification
zbMATH Keywords: equational theories
zbMATH Keywords: automated deduction
zbMATH Keywords: associative- commutative functions
zbMATH Keywords: homogeneous linear diophantine equations
zbMATH Keywords: termination
zbMATH Keywords: correctness
MaRDI profile type: Publication
Wikidata QID: Q56092434
cites work: Q3696522
cites work: Hilbert's Tenth Problem is Unsolvable
cites work: On the sequential nature of unification
cites work: Complete sets of unifiers and matchers in equational theories
cites work: Q3703287
cites work: Q3786019
cites work: An algorithm to generate the basis of solutions to homogeneous linear Diophantine equations
cites work: Q3219154
cites work: Q4159542
cites work: An Efficient Unification Algorithm
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Q5678447
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: A Unification Algorithm for Associative-Commutative Functions
cites work: Q3785922
cites work: Q3716322
DBLP publication ID: journals/jsc/Fages87
description: scientific article; zbMATH DE number 4041329