diff options
Diffstat (limited to 'content/zettel/4e1.md')
| -rw-r--r-- | content/zettel/4e1.md | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/content/zettel/4e1.md b/content/zettel/4e1.md new file mode 100644 index 0000000..71407e9 --- /dev/null +++ b/content/zettel/4e1.md @@ -0,0 +1,19 @@ ++++ +title = "Craig interpolation" +author = "Yann Herklotz" +tags = [] +categories = [] +backlinks = ["4e", "3a8g5h2"] +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. |