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 Both sides next revision
sav08:normal_forms_for_propositional_logic [2008/03/09 12:45]
thibaud Filled-in negation-normal paragraph
sav08:normal_forms_for_propositional_logic [2008/03/09 13:25]
thibaud Filled-in DNF
Line 18: Line 18:
  
 === Disjunctive Normal Form === === Disjunctive Normal Form ===
 +Formulas in Disjunctive-normal form look like this: 
 +$(x_1 \land x_2 \land \lnot x_3) \lor (\lnot x_1 \land x_3 \land x_4) \lor ...$ \\
 +More formally $F = \bigvee^{n}_{i=1} D_i$ where $n \geq 0$. \\
 +Each $D_i$ is a clause and is defined as $D_i = \bigwedge_{j=1}^{n_i} L_{ij}$. \\
 +Each $L_{ij}$ is a literal. It's either an elementary proposition or its negation.
  
-Complete disjunctive normal form and truth tables+Solving the SAT problem for DNF formulas is in P, but transforming an arbitrary propositional formula to DNF causes an exponential blow-up
-  * generating ​DNF from truth table + 
-  * generating DNF by transformations+DNF formulas can be easily generated ​from truth tables. Each row of the truth table that makes the formula true can be written as a clause. For a formula over $n$ variables, there are $2^{n}$ rows in the truth table. Over $n$ variables, there are $2^{2^{n}}$ different (i.e. non-equivalent) formulas.
  
 === Conjunctive Normal Form === === Conjunctive Normal Form ===