Winkler, F.; Buchberger, B. 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. Cited in 20 Documents MSC: 03B35 Mechanization of proofs and logical operations 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 08B05 Equational logic, Mal’tsev conditions Keywords:word problems; completion procedure; equational theory; generalized Newman lemma; Church-Rosser property; reduction relations Citations:Zbl 0593.00024 PDFBibTeX XML