Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:fixed-width_bitvectors [2008/03/13 19:22] vkuncak |
sav08:fixed-width_bitvectors [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 26: | Line 26: | ||
| We present translation from $F$ to equisatisfiable $prop(F)$ in propositional logic. That is, | We present translation from $F$ to equisatisfiable $prop(F)$ in propositional logic. That is, | ||
| - | \[ | + | \begin{equation*} |
| \exists x_1,\ldots,x_n.\ F | \exists x_1,\ldots,x_n.\ F | ||
| - | \] | + | \end{equation*} |
| is equivalent to | is equivalent to | ||
| - | \[ | + | \begin{equation*} |
| \exists p_1,\ldots,p_m.\ prop(F) | \exists p_1,\ldots,p_m.\ prop(F) | ||
| - | \] | + | \end{equation*} |
| Where $FV(F)=\{x_1,\ldots,x_n\}$ and $FV(prop(F)) = \{p_1,\ldots,p_m\}$. | Where $FV(F)=\{x_1,\ldots,x_n\}$ and $FV(prop(F)) = \{p_1,\ldots,p_m\}$. | ||