Skip to Main content Skip to Navigation
Conference papers

A Generic Framework for Implicate Generation Modulo Theories

Mnacho Echenim 1 Nicolas Peltier 1 Yanis Sellami 1
1 CAPP - Calculs algorithmes programmes et preuves
LIG - Laboratoire d'Informatique de Grenoble [2007-2015]
Abstract : The clausal logical consequences of a formula are called its implicates. The generation of these implicates has several applications, such as the identification of missing hypotheses in a logical specification. We present a procedure that generates the implicates of a quantifier-free formula modulo a theory. No assumption is made on the considered theory, other than the existence of a decision procedure. The algorithm has been implemented (using the solvers MiniSAT, CVC4 and Z3) and experimental results show evidence of the practical relevance of the proposed approach.
Complete list of metadatas

Cited literature [32 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01833514
Contributor : Yanis Sellami <>
Submitted on : Thursday, November 7, 2019 - 9:41:47 AM
Last modification on : Thursday, July 9, 2020 - 9:44:46 AM
Document(s) archivé(s) le : Saturday, February 8, 2020 - 9:19:33 PM

File

paper_42.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01833514, version 1

Collections

Citation

Mnacho Echenim, Nicolas Peltier, Yanis Sellami. A Generic Framework for Implicate Generation Modulo Theories. IJCAR, Jul 2018, Oxford, United Kingdom. ⟨hal-01833514⟩

Share

Metrics

Record views

149

Files downloads

114