# A Generic Framework for Implicate Generation Modulo Theories

arXiv: https://arxiv.org/abs/1807.04557 · HTML: https://mlsanity.com/paper/1807.04557/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 12 Jul 2018.

## Built on by (most cited first, 2 of 2)

- [Connection-minimal Abduction in EL via Translation to FOL -- Technical Report](https://mlsanity.com/paper/2205.08449/) (2022)
- [Bridging the Gap Between Scientific Laws Derived by AI Systems and Canonical Knowledge via Abductive Inference with AI-Noether](https://mlsanity.com/paper/2509.23004/) (2025)

## Abstract (arXiv)

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.