+++
title = "Craig interpolation"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["4e", "3a8g5h2", "3a8g5h"]
forwardlinks = ["4e2"]
zettelid = "4e1"
+++

Craig interpolation is an interesting method used in model checkers to
generate intermediate propositions that only contain the atoms of the
intersection between the other propositions in the implication.

The idea is that if one has $p \rightarrow q$, then one can generate
$p\rightarrow c \rightarrow q$, where $a(c) = a(p) \cap a(q)$. This
means that one can generate a more minimal proposition that still
captures the important information. However, without adding quantifiers,
it's not possible to remove atoms without breaking strict equivalence.