# Converting from formula to clause

I'm trying to refresh myself on the subject.

If φ= (L1 ∨...∨ Ln) whereL1,...,Ln are literals, then{L1, ..., Ln}is the clause associated to φ.

How would I convert ¬(¬P ∨ Q) to a clause?

$$\neg (\neg P \lor Q) \Leftrightarrow \neg \neg P \land \neg Q \Leftrightarrow P \land \neg Q$$
Now that it is in CNF, you know that each conjunct is a generalized disjunction that can be made into a clause. In this case, you have two conjuncts, so you will get two clauses: $$\{ P \}$$ and $$\{ \neg Q \}$$