LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:interpolation_for_propositional_logic [2008/03/10 11:30]
vkuncak
sav08:interpolation_for_propositional_logic [2008/03/17 20:24]
piskac
Line 1: Line 1:
 ====== Interpolation for Propositional Logic ====== ====== Interpolation for Propositional Logic ======
  
-Given two propositional formulas $F$ and $G$, an interpolant for $(F,G)$ is a propositional formula $H$ such that: \\+**Definition of Interpolant:​** 
 +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$ \\
 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 formulasee [[Propositional Logic Syntax]]. 
 +++++
  
-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]]):​+Note that $F \rightarrow G$ by transitivity of $\rightarrow$. The interpolant ​extracts the essential part of formula $F$ which makes $F$ imply $G$. 
 + 
 +Let $elim$ denote the operator that eliminates propositional quantifiers (see [[QBF and Quantifier Elimination]])
 + 
 +Here are two **simple ways to construct an interpolant:**
   * We can quantify existentially all variables in $F$ that are not in $G$.   * We can quantify existentially all variables in $F$ that are not in $G$.
  
Line 17: Line 23:
   * We can quantify universally all variables in $G$ that are not in $F$.   * We can quantify universally all variables in $G$ that are not in $F$.
  
-$H_{max} \equiv elim(\forall ​p_1p_2, ..., p_n.\ G)$ where $\{p_1p_2, ..., p_n \}\ = FV(G)\backslash FV(F)$ \\+$H_{max} \equiv elim(\forall ​q_1q_2, ..., q_m.\ G)$ where $\{q_1q_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)$ \}
 \] \]
-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)$