Only prime superpositions need be considered in the Knuth-Bendix completion procedure
type: Item
instance of: scholarly article
title: Only prime superpositions need be considered in the Knuth-Bendix completion procedure
zbMATH Open document ID: 0651.68029
DOI: 10.1016/S0747-7171(88)80019-1
author: Deepak Kapur
author: David R. Musser
author: Paliath Narendran
published in: Journal of Symbolic Computation
publication date: 1988-01-01T00:00:00Z
review text: The Knuth and Bendix test for local confluence of a term rewriting system involves generating superpositions of the left-hand sides, and for each superposition deriving a critical pair of terms and checking whether these terms reduce to the same term. We prove that certain superpositions, which are called composite because they can be split into other superpositions, do not have to be subjected to the critical-pair- joinability test; it suffices to consider only prime superpositions. As a corollary, this result settles a conjecture of Lankford that unblocked superpositions can be omitted. To prove the result, we introduce new concepts and proof techniques which appear useful for other proofs relating to the Church-Rosser property. This test has been implemented in the completion procedures for ordinary term rewriting systems as well as term rewriting systems with associative-commutative operators. Performance of the completion procedures with this test and without the test are compared on a number of examples in the Rewrite Rule Laboratory (RRL) being developed at General Electric Research and Development Center.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68W30
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4062564
zbMATH Keywords: Knuth-Bendix completion
zbMATH Keywords: term rewriting system
zbMATH Keywords: critical pair
zbMATH Keywords: prime superpositions
zbMATH Keywords: Church-Rosser property
describes a project that uses: RRL
describes a project that uses: REVE
MaRDI profile type: Publication
cites work: Non-resolution theorem proving
cites work: Q3208084
cites work: Proving termination with multiset orderings
cites work: Q3338216
cites work: Q3703287
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Proof by consistency
cites work: Q3783519
cites work: Q5581665
cites work: Q3702510
cites work: Abstract Data Type Specification in the Affirm System
cites work: Q3687693
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
cites work: A Unification Algorithm for Associative-Commutative Functions
cites work: Q3745825
cites work: Q3675515
description: scientific article; zbMATH DE number 4062564