A complete proof of correctness of the Knuth-Bendix completion algorithm
type: Item
instance of: scholarly article
title: A complete proof of correctness of the Knuth-Bendix completion algorithm
zbMATH Open document ID: 0465.68014
DOI: 10.1016/0022-0000(81)90002-7
author: Gérard Huet
published in: Journal of Computer and System Sciences
publication date: 1981-01-01T00:00:00Z
full work available at URL: RR-0025.pdf
Mathematics Subject Classification ID: 68W99
Mathematics Subject Classification ID: 03B25
Mathematics Subject Classification ID: 08A99
Mathematics Subject Classification ID: 68Q65
zbMATH DE Number: 3729441
zbMATH Keywords: semidecision algorithm
zbMATH Keywords: validity problem in equational theories
zbMATH Keywords: decision procedure
zbMATH Keywords: term rewriting
Wikidata QID: Q55952378
MaRDI profile type: Publication
OpenAlex ID: W1991856459
cites work: New decision algorithms for finitely presented commutative semigroups
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Q5581665
cites work: Complete Sets of Reductions for Some Equational Theories
description: scientific article; zbMATH DE number 3729441