CC(X): Semantic Combination of Congruence Closure with Solvable Theories | Zendy

Sylvain Conchon | Zendy; Évelyne Contejean | Zendy; Johannes Kanig | Zendy; Stéphane Lescuyer | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

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

Author(s) -

Sylvain Conchon,

Évelyne Contejean,

Johannes Kanig,

Stéphane Lescuyer

Publication year - 2008

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2008.04.080

Subject(s) - congruence (geometry) , modulo , closure (psychology) , core (optical fiber) , class (philosophy) , discrete mathematics , mathematics , computer science , algorithm , theoretical computer science , artificial intelligence , law , telecommunications , geometry , political science

We present a generic congruence closure algorithm for deciding ground formulas in the combination of the theory of equality with uninterpreted symbols and an arbitrary built-in solvable theory X. Our algorithm CC(X) is reminiscent of Shostak combination: it maintains a union-find data-structure modulo X from which maximal information about implied equalities can be directly used for congruence closure. CC(X) diverges from Shostak's approach by the use of semantic values for class representatives instead of canonized terms. Using semantic values truly reflects the actual implementation of the decision procedure for X. It also enforces to entirely rebuild the algorithm since global canonization, which is at the heart of Shostak combination, is no longer feasible with semantic values. CC(X) has been implemented in Ocaml and is at the core of Ergo, a new automated theorem prover dedicated to program verification

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research