We describe an implementation of the KNS ordering within the TRIP system, a Quintus-Prolog written laboratory for experimenting with new rewrite-like approaches to theorem proving in first-order logic. The aim of the TRIP system is not to obtain high-performance theorem provers, but rather to test techniques that could be the basis for such theorem provers. The KNS ordering is a partial ordering scheme for proving the uniform termination of term rewriting systems, which is a crucial aspect of Knuth-Bendix completion-like theorem proving procedures. The KNS ordering is used within TRIP as a subsystem of a very general completion procedure for first-order clauses with equality, based on recent work done in this field by Bachmair and Ganzinger (1990,1991) subsuming and generalizing many known results. Our system contributes to the further development of these methods in several ways, and especially w.r.t. the definition of new techniques which are necessary for exploiting in their full power the redundancy notions that have now become available. We apply results from, where a highly simplified framework for defining Knuth-Bendix-like completion procedures for full first order clauses with equality is defined and instantiated by a new, simpler and more restrictive inference system. This implementation uses the notion of clausal rewriting (Nieuwenhuis and Orejas, 1991) for the definition of a single formalized method for proving the redundancy of clauses and inferences.
