A Generic Framework for Implicate Generation Modulo Theories

TL;DR

This paper introduces a generic algorithm for generating implicates of quantifier-free formulas within various theories, leveraging existing decision procedures and demonstrating practical effectiveness through implementation with multiple solvers.

Contribution

It presents a theory-agnostic framework for implicate generation that works with any decidable theory, extending the applicability of logical consequence analysis.

Findings

Algorithm successfully implemented with MiniSat, CVC4, and Z3.

Experimental results confirm practical relevance and efficiency.

Framework applicable to a wide range of theories.

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.