Lab for Automated Reasoning and Analysis 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/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:
 
sav08/interpolation_for_propositional_logic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice