HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Congruence Closure modulo Associativity-Commutativity

Leo Bachmair 1 I. V. Ramakrishnan 1 Ashish Tiwari 1 Laurent Vigneron 2
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We introduce the notion of an associative-commutative congruence closure and show how such closures can be constructed via completion-like transition rules. This method is based on combining completion algorithms for theories over disjoint signatures to produce a convergent system over an extended signature. This approach can also be used to solve the word problem for ground AC-theories without using AC-simplification orderings. We also discuss transformation of a convergent system over an extended signature to a convergent system (modulo AC) over the original signature.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:51:48 AM
Last modification on : Friday, February 4, 2022 - 3:24:56 AM


  • HAL Id : inria-00099214, version 1



Leo Bachmair, I. V. Ramakrishnan, Ashish Tiwari, Laurent Vigneron. Congruence Closure modulo Associativity-Commutativity. 3rd International Workshop on Frontiers of Combining Systems - FroCoS'2000, Mar 2000, Nancy, France, pp.242-256. ⟨inria-00099214⟩



Record views