Critical pair criteria for completion
type: Item
instance of: scholarly article
title: Critical pair criteria for completion
zbMATH Open document ID: 0651.68030
DOI: 10.1016/S0747-7171(88)80018-X
author: Leo Bachmair
author: Nachum Dershowitz
published in: Journal of Symbolic Computation
publication date: 1988-01-01T00:00:00Z
review text: We formulate the Knuth-Bendix completion method at an abstract level, as an equational inference system, and formalize the notion of critical pair criterion using orderings on equational proofs. We prove the correctness of standard completion and verify all known criteria for completion, including those for which correctness had not been established previously. What distinguishes our approach from others is that our results apply to a large class of completion procedures, not just to a particular version. Proof ordering techniques therefore provide a basis for the design and verification of specific completion procedures (with or without criteria).
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4062565
zbMATH Keywords: Knuth-Bendix completion
zbMATH Keywords: equational inference system
zbMATH Keywords: critical pair
zbMATH Keywords: orderings on equational proofs
MaRDI profile type: Publication
cites work: Q3809306
cites work: Q3208084
cites work: Q3336682
cites work: Computing with rewrite systems
cites work: Proving termination with multiset orderings
cites work: Refutational theorem proving using term-rewriting systems
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: A complete proof of correctness of the Knuth-Bendix completion algorithm
cites work: Proofs by induction in equational theories with constructors
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Q5581665
cites work: Q3702510
cites work: Q3993260
cites work: Q3992832
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
cites work: Q3675515
cites work: Q3702509
cites work: Q3745825
description: scientific article; zbMATH DE number 4062565