Unfailing completion is a commonly used technique for equational reasoning. For equational problems with associative and commutative functions, unfailing completion often generates a large number of rewrite rules. By comparing it with a ground compeltion procedure, we show that many of the rewrite rules generated are redundant. A set of consistency constraints is formualted to detect redundant rewrite rules. We propsoe a new completion algorithm, consistent unfailing completion, in which only consistent rewrite rules are used for critical pair generation and rewriting. Our approach does nto need to use flattened terms. Thus it avoids the double exponential worst case complexity of AC unifcation. It also allows the use of more flexible termination orderings. We present some sufficient conditions for detecting inconsistent rewrite rules. The proposed algorithm is implemented in PROLOG.
展开▼
