Congruence Closure with Free Variables (Work in Progress) - Archive ouverte HAL Access content directly
Conference Papers Year : 2015

Congruence Closure with Free Variables (Work in Progress)

(1) , (1)
1

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.
Fichier principal
Vignette du fichier
BarbosaFontaine-QUANTIFY2015.pdf (333.14 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01246036 , version 1 (18-12-2015)

Identifiers

  • HAL Id : hal-01246036 , version 1

Cite

Haniel Barbosa, Pascal Fontaine. Congruence Closure with Free Variables (Work in Progress). QUANTIFY 2015 - 2nd International Workshop on Quantification, Aug 2015, Berlin, Germany. ⟨hal-01246036⟩
165 View
160 Download

Share

Gmail Facebook Twitter LinkedIn More