Convert a FOL formula into CNF

441 Views Asked by At
∀x (¬Strike(x) ∨ Contract(x)) ⇒Report(x) 

Eliminate ⇒

∀x ¬(¬Strike(x) ∨ Contract(x))∨Report(x) 

Push negation inside

∀x Strike(x) ∧¬Contract(x)∨Report(x) 

is this correct?

1

There are 1 best solutions below

0
On

The procedure is not wrong, although the names for the justification names are off.   Well, it is clear what you mean, so that's not too wrong.   However, it is better to get the terminology down.

Additionally, to derive a Conjunctive Normal Form you need just one more step. You want a conjunction of disjuncts.

$$\def\Strike{\operatorname{Strike}}\def\Contract{\operatorname{Contract}}\def\Report{\operatorname{Report}} {\forall x~(\neg\Strike(x) \lor \Contract(x)~\to~ \Report(x))\\\quad\Updownarrow\quad\text{Implication Equivalence}\\\forall x~(\neg(\neg\Strike(x)\lor\Contract(x))\lor\Report(x))\\\quad\Updownarrow\quad\text{de Morgan's Duality}\\\forall x~((\Strike(x)\land\neg\Contract(x))\lor\Report(x))\\\quad\Updownarrow\quad\text{Distribution}\\\bbox[border:dotted navy 1pt]{\phantom{\forall x~((\Strike(x)\lor\Report(x))\land(\neg\Contract(x)\lor\Report(x)))}}}$$