scholarly journals CC(X): Semantic Combination of Congruence Closure with Solvable Theories

2008 ◽  
Vol 198 (2) ◽  
pp. 51-69 ◽  
Author(s):  
Sylvain Conchon ◽  
Evelyne Contejean ◽  
Johannes Kanig ◽  
Stéphane Lescuyer
Keyword(s):  
Congruence Closure

scholarly journals Fast congruence closure and extensions

2007 ◽  
Vol 205 (4) ◽  
pp. 557-580 ◽  
Author(s):  
Robert Nieuwenhuis ◽  
Albert Oliveras
Keyword(s):  
Congruence Closure

Definability properties and the congruence closure

1990 ◽  
Vol 30 (4) ◽  
pp. 231-240 ◽  
Author(s):  
Xavier Caicedo
Keyword(s):  
Congruence Closure

scholarly journals A Data Structure to Handle Large Sets of Equal Terms

10.29007/hsbm ◽  
2018 ◽  
Author(s):  
Baudouin Le Charlier ◽  
Mêton Mêton Atindehou
Keyword(s):  
Data Structure ◽  
Complexity Analysis ◽  
Formal Theory ◽  
Experimental Results ◽  
Main Motivation ◽  
Large Sets ◽  
Congruence Closure ◽  
Definition Of

We present a data structure to represent and manipulate large sets of (equal) terms (or expressions). Our initial and main motivation for this data structure is the simplification of expressions with respect to a formal theory, typically, an equational one. However, it happens that the data structure is also efficient to compute the congruence closure of a relation over a set of terms.We provide an abstract definition of the data structure, including a precise semantics, and we explain how to implement it efficiently. We prove the correctness of the proposed algorithms, with a complexity analysis and experimental results. We compare these algorithms with previous algorithms to compute the congruence closure and we also sketch how we use the data structure to tackle the expression simplification problem.

Sign in / Sign up

Export Citation Format

Share Document