Equational methods in first order predicate calculus
The author translates proof procedures (e.g. resolution and narrowing) in quantifier free first order logic (and not in full first order logic as announced in the title) into equational rewriting systems and investigates (partial) confluence and the appropriate modification of the Knuth-Bendix completion algorithm in this context.
scientific article; zbMATH DE number 3922617
scientific article