Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:normal_forms_for_propositional_logic [2008/03/09 15:39] thibaud Filled-in SAT preserving transformation to CNF |
sav08:normal_forms_for_propositional_logic [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 4: | Line 4: | ||
In Negation-normal from, negations are only allowed on elementary proposition. Moreover, NNF formulas contain no implication, so the only binary operators are conjunctions and disjunctions. The following rules can be used to turn arbitrary propositional formulas into negation-normal form. | In Negation-normal from, negations are only allowed on elementary proposition. Moreover, NNF formulas contain no implication, so the only binary operators are conjunctions and disjunctions. The following rules can be used to turn arbitrary propositional formulas into negation-normal form. | ||
- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
\lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\ | \lnot (p \land q) \leftrightarrow (\lnot p) \lor (\lnot q) \\ | ||
p \leftrightarrow \lnot (\lnot p) \\ | p \leftrightarrow \lnot (\lnot p) \\ | ||
Line 10: | Line 10: | ||
\lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) | \lnot (p \lor q) \leftrightarrow (\lnot p) \land (\lnot q) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
Note that this transformation is linear in the size of the formula. No exponential blow-up. | Note that this transformation is linear in the size of the formula. No exponential blow-up. | ||
Line 73: | Line 73: | ||
The key transformation steps are: | The key transformation steps are: | ||
- | \[\begin{array}{l} | + | \begin{equation*}\begin{array}{l} |
F\ \ \leadsto\ \ (p_i \leftrightarrow (q \land r)) \land subst(\{q \land r \mapsto p_i\},F) \\ | F\ \ \leadsto\ \ (p_i \leftrightarrow (q \land r)) \land subst(\{q \land r \mapsto p_i\},F) \\ | ||
F\ \ \leadsto\ \ (p_i \leftrightarrow (q \lor r)) \land subst(\{q \lor r \mapsto p_i\},F) \\ | F\ \ \leadsto\ \ (p_i \leftrightarrow (q \lor r)) \land subst(\{q \lor r \mapsto p_i\},F) \\ | ||
F\ \ \leadsto\ \ (p_i \leftrightarrow (\lnot q)) \land subst(\{(\lnot q) \mapsto p_i\},F) \\ | F\ \ \leadsto\ \ (p_i \leftrightarrow (\lnot q)) \land subst(\{(\lnot q) \mapsto p_i\},F) \\ | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
Each equivalence between a representative and the ones from the sub-formulas has to be flatten to conjunctive-normal form. This can be done by splitting the equivalences into two implications. Example: \\ | Each equivalence between a representative and the ones from the sub-formulas has to be flatten to conjunctive-normal form. This can be done by splitting the equivalences into two implications. Example: \\ |