×

A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. (English) Zbl 0607.03003

Algebra, combinatorics and logic in computer science, Colloq. Györ/Hung. 1983, Vol. 2, Colloq. Math. Soc. János Bolyai 42, 849-869 (1986).
[For the entire collection see Zbl 0593.00024.]
Given a finite set E of equations between first-order terms, the Knuth- Bendix procedure (if it succeeds) constructs a set E’ of equations such that E and E’ generate the same equational theory and equality modulo this equational theory can be decided by reduction to normal forms with respect to E’ (the equations in E’ are considered as rewrite rules). In this paper it is shown that certain computations in the Knuth-Bendix procedure can be eliminated by an a-priori criterion based on a certain ”overlap condition”. As a general framework for correctness proofs of refined versions of the Knuth-Bendix procedure a generalized Newman lemma is proven that establishes the Church-Rosser property for reduction relations under a very weak hypothesis.

MSC:

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
08B05 Equational logic, Mal’tsev conditions

Citations:

Zbl 0593.00024