LARA

Differences

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

Link to this comparison view

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: \\