Abstract Congruence Closure

We describe the concept of an Abstract Congruence Closure and provide equational inference rules for its construction. The length of any maximal derivation using these inference rules for constructing an Abstract Congruence Closure is at most quadratic in the input size. The framework is used to des...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2003-01, Vol.31 (2), p.129-168
Main Authors: Bachmair, Leo, Tiwari, Ashish, Vigneron, Laurent
Format: Article
Language:English
Subjects:
Algorithms
Closures
Computer Science
Congruences
Construction
Grounds
Inference
Mathematical analysis
Other
Studies
Symbols
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We describe the concept of an Abstract Congruence Closure and provide equational inference rules for its construction. The length of any maximal derivation using these inference rules for constructing an Abstract Congruence Closure is at most quadratic in the input size. The framework is used to describe the logical aspects of some well-known algorithms for congruence closure. It is also used to obtain an efficient implementation of congruence closure. We present experimental results that illustrate the relative differences in performance of the different algorithms. The notion is extended to handle associative and commutative function symbols, thus providing the concept of an associative-commutative congruence closure. Congruence closure (modulo associativity and commutativity) can be used to construct ground convergent rewrite systems corresponding to a set of ground equations (containing AC symbols).[PUBLICATION ABSTRACT]
ISSN:0168-7433
1573-0670
DOI:10.1023/B:JARS.0000009518.26415.49