| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Congruence Closure with Free Variables (Work in Progress)
Abstract : This paper presents preliminary work on the definition of a general framework for handling quantified formulas in SMT solving. Its focus is on the derivation of instances conflicting with a ground context, redefining the approach introduced in [11]. An enhanced version of the classical congruence closure algorithm, able to handle free variables, is presented.
Cited literature [12 references]
https://hal.inria.fr/hal-01246036
Contributor : Pascal Fontaine <>
Submitted on : Friday, December 18, 2015 - 10:21:58 AM
Last modification on : Tuesday, December 8, 2020 - 10:19:47 AM
Long-term archiving on: : Saturday, April 29, 2017 - 8:37:22 PM
Contributor : Pascal Fontaine <>
Submitted on : Friday, December 18, 2015 - 10:21:58 AM
Last modification on : Tuesday, December 8, 2020 - 10:19:47 AM
Long-term archiving on: : Saturday, April 29, 2017 - 8:37:22 PM
File
BarbosaFontaine-QUANTIFY2015.p...
Files produced by the author(s)