We present an abstract completion-based method for finding normal forms of terms with respect to given rewrite systems.The method uses the conecpt of a rewrite closure,which is a generalization of the idea of a congruence closure.Our results generalize previous results on congruence closure-based normalization methods.The description of known methods within our formalism also allows a better understanding of these procedures.
展开▼
