Sciweavers

IJCAI
1997

Equational Reasoning using AC Constraints

13 years 11 months ago
Equational Reasoning using AC Constraints
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 completion procedure, we show that many of the rewrite rules generated are redundant. A set of consistency constraints is formulated to detect redundant rewrite rules. We propose a new completion algorithm, consistent unfailing completion, in which only consistent rewrite rules are used for critical pair generation and rewriting. Our approach does not need to use flattened terms. Thus it avoids the double exponential worst case complexity of AC unification. 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.
David A. Plaisted, Yunshan Zhu
Added 01 Nov 2010
Updated 01 Nov 2010
Type Conference
Year 1997
Where IJCAI
Authors David A. Plaisted, Yunshan Zhu
Comments (0)