• English only

Differences

This shows you the differences between two versions of the page.

sav08:interpolation_for_propositional_logic [2008/03/11 16:18]
vkuncak
sav08:interpolation_for_propositional_logic [2015/04/21 17:30] (current)
Line 2: Line 2:

**Definition of Interpolant:​** **Definition of Interpolant:​**
-Given two propositional formulas $F$ and $G$, an interpolant for $(F,G)$ is a propositional formula $H$ such that: \\+Given two propositional formulas $F$ and $G$, such that $\models F \rightarrow ​G$, an interpolant for $(F,G)$ is a propositional formula $H$ such that: \\
1) $\models F \rightarrow H$ \\ 1) $\models F \rightarrow H$ \\
2) $\models H \rightarrow G$ \\ 2) $\models H \rightarrow G$ \\
Line 26: Line 26:

**Definition:​** ${\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,
-$+\begin{equation*} {\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) \} -$+\end{equation*}

**Theorem:​** The following properties hold for $H_{min}$, $H_{max}$, ${\cal I}(F,G)$ defined above: **Theorem:​** The following properties hold for $H_{min}$, $H_{max}$, ${\cal I}(F,G)$ defined above: