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.
CITATION STYLE
Echenim, M., Peltier, N., & Sellami, Y. (2018). A Generic Framework for Implicate Generation Modulo Theories. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10900 LNAI, pp. 279–294). Springer Verlag. https://doi.org/10.1007/978-3-319-94205-6_19
Mendeley helps you to discover research relevant for your work.