Completion to Strongly Confluent Term Rewriting Systems

Abstract

In a landmark 1970 paper, Knuth and Bendix introduced completion method to (try to) transform a set of equations E into a confluent and terminating Term Rewriting System (TRS) R_E. If the transformation successfully finishes, since R_E is confluent and terminating, it can be used to prove and disprove equational goals $u=v$ by just checking whether the (computable and unique) normal forms u' and v' of u and v are identical or not. In a previous paper, we have developed and implemented a method to prove and disprove the validity of equations with respect to E using confluent but possibly nonterminating TRSs R_E. In this paper we discuss completion procedures to obtain strongly confluent, not necessarily terminating, TRSs R_E from a set of equations E. Strong confluence implies confluence without requiring termination. Our techniques have been implemented as part of the tool TRS.Tool. We show its performance by means of some benchmarks.