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
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


Files produced by the author(s)


  • HAL Id : hal-01833514, version 1



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



Record views


Files downloads