Abstract:

Abstract:
We suggest a proof-theoretical setting in which 
completion processes, as used for equational reasoning, can
be modeled and generalized. This framework
-- based on a well-founded ordering on proofs -- allows one to derive
redundancy criteria and saturation processes abstractly.