Generic Completion (Version 1)

Abstract rewrite systems define a reduction relation by a set of rules. An important aspect of such rewrite relations is their behavior in an arbitrary context associated with the underlying congruence relation. This behavior is described by "compatibility properties": a rewrite system is compatible if applying the same context to two objects preserves the rewrite relation among them. We present a generic completion procedure for abstract rewrite systems and characterize the minimal compatibility requirement for rewrite relations that are necessary to describe completion procedures as proof transformation procedures. This requirement (called sufficient compatibility) subsumes the class of semi-compatible rewrite relations that play an important role in algebraic completion. In order to allow for non-compatible rewrite relations we must replace the concept of equations (critical pairs) by promises which leads to a new proof transformation relation and a new proof ordering for abstract r..