Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:interpolation_for_propositional_logic [2008/03/10 11:22] vkuncak |
sav08:interpolation_for_propositional_logic [2008/03/11 16:15] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Interpolation for Propositional Logic ====== | ====== Interpolation for Propositional Logic ====== | ||
+ | **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$, an interpolant for $(F,G)$ is a propositional formula $H$ such that: \\ | ||
1) $\models F \rightarrow H$ \\ | 1) $\models F \rightarrow H$ \\ | ||
Line 6: | Line 7: | ||
3) $FV(H)\subseteq FV(F) \cap FV(G)$ | 3) $FV(H)\subseteq FV(F) \cap FV(G)$ | ||
- | $FV$ denotes the set of free variables in the given propositional formula (see [[Propositional Logic Syntax]]). | + | ++++What is FV?| |
+ | $FV$ denotes the set of free variables in the given propositional formula, see [[Propositional Logic Syntax]]. | ||
+ | ++++ | ||
Note that $F \rightarrow G$ by transitivity of $\rightarrow$. The interpolant extracts what makes $F$ imply $G$. | Note that $F \rightarrow G$ by transitivity of $\rightarrow$. The interpolant extracts what makes $F$ imply $G$. | ||
- | Here are two easy ways to create an interpolant. Let $elim$ denote the operator that eliminates propositional quantifiers (see [[QBF and Quantifier Elimination]]): | + | Let $elim$ denote the operator that eliminates propositional quantifiers (see [[QBF and Quantifier Elimination]]). |
- | * We can quantify existentially all variables in $F$ that are not in $G$. We obtain the //weakest interpolant//: | + | |
+ | Here are two simple ways to construct an interpolant: | ||
+ | * We can quantify existentially all variables in $F$ that are not in $G$. | ||
$H_{min} \equiv elim(\exists p_1, p_2, ..., p_n.\ F)$ where $\{p_1, p_2, ..., p_n \}\ = FV(F)\backslash FV(G)$ \\ | $H_{min} \equiv elim(\exists p_1, p_2, ..., p_n.\ F)$ where $\{p_1, p_2, ..., p_n \}\ = FV(F)\backslash FV(G)$ \\ | ||
- | * We can quantify universally all variables in $G$ that are not in $F$. We obtain the //strongest interpolant//: | + | * We can quantify universally all variables in $G$ that are not in $F$. |
- | $H_{max} \equiv elim(\forall p_1, p_2, ..., p_n.\ G)$ where $\{p_1, p_2, ..., p_n \}\ = 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, | More precisely, let ${\cal I}(F,G)$ denote the set of all interpolants for $(F,G)$, that is, |