Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:interpolation_for_propositional_logic [2008/03/11 16:16] vkuncak |
sav08:interpolation_for_propositional_logic [2008/03/11 16:18] vkuncak |
||
|---|---|---|---|
| Line 25: | Line 25: | ||
| $H_{max} \equiv elim(\forall q_1, q_2, ..., q_m.\ G)$ where $\{q_1, q_2, ..., q_m \}\ = FV(G)\backslash FV(F)$ \\ | $H_{max} \equiv elim(\forall q_1, q_2, ..., q_m.\ G)$ where $\{q_1, q_2, ..., q_m \}\ = FV(G)\backslash FV(F)$ \\ | ||
| - | More precisely, let ${\cal I}(F,G)$ denote the set of all interpolants for $(F,G)$, that is, | + | **Definition:** ${\cal I}(F,G)$ denote the set of all interpolants for $(F,G)$, that is, |
| \[ | \[ | ||
| {\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \} | {\cal I}(F,G) = \{ H \mid H \mbox{ is interpolant for $(F,G)$ \} | ||
| \] | \] | ||
| - | **Theorem:** Then the following properties hold: | + | **Theorem:** The following properties hold for $H_{min}$, $H_{max}$, ${\cal I}(F,G)$ defined above: |
| - $H_{min} \in {\cal I}(F,G)$ | - $H_{min} \in {\cal I}(F,G)$ | ||
| - $\forall H \in {\cal I}(F,G).\ \models (H_{min} \rightarrow H)$ | - $\forall H \in {\cal I}(F,G).\ \models (H_{min} \rightarrow H)$ | ||