next up previous
Next: About this document ... Up: predCalc Previous: Predicate Calculus Example (p.

Putting a Formula into Clause Form (p. 285 Tanimoto)


\begin{displaymath}(\forall x){P(x) \rightarrow (\exists y){Q(x,y)}} \bigwedge (\forall x){\neg P(x) \rightarrow \neg (\exists y){Q(x,y)}}\end{displaymath}

Step 1: Eliminate implications

\begin{displaymath}(\forall x){\neg P(x) \bigvee (\exists y){Q(x,y)}} \bigwedge (\forall x){\neg \neg P(x) \bigwedge \neg (\exists y){Q(x,y)}}\end{displaymath}

Step 2: Reduce the scope of each negation sign. Use DeMorgans if possible Also use:

\begin{displaymath}\neg (\forall x)P(x) iff (\exists x) \neg P(x)\end{displaymath}


\begin{displaymath}\neg (\exists x)P(x) iff (\forall x) \neg P(x)\end{displaymath}

Also reduce any double negatives.

\begin{displaymath}(\forall x){\neg P(x) \bigvee (\exists y){Q(x,y)}} \bigwedge (\forall x){P(x) \bigvee (\forall y){\neg Q(x,y)}}\end{displaymath}

Step 3: Standardize the variables of the formula, giving each quantifier a different name.

\begin{displaymath}(\forall x){\neg P(x) \bigvee (\exists y){Q(x,y)}} \bigwedge (\forall z){P(z) \bigvee (\forall w){not Q(z,w)}}\end{displaymath}

Step 4: Eliminate the existential quantifiers using Skolemization

\begin{displaymath}(\forall x){\neg P(x) \bigvee Q(x,f(x))} \bigwedge (\forall z){P(z) \bigvee (\forall w){\neg Q(z,w)}}\end{displaymath}

Step 5: Remove the universal quantifiers

\begin{displaymath}{\neg P(x) \bigvee Q(x, f(x))} \bigwedge {P(z) \bigvee \neg Q(z,w)}\end{displaymath}

Step 6: Put into conjuntive normal form (This function already is)

Distributive Laws may be helpful:

\begin{displaymath}P \bigvee (Q \bigwedge R) = (P \bigvee Q) \bigwedge (R \bigvee R)\end{displaymath}


\begin{displaymath}P \bigwedge (Q \bigvee R) = (P \bigwedge Q) \bigvee (P \bigwedge R)\end{displaymath}

Step 7: Separate the conjucts into separate clauses:

\begin{displaymath}\neg P(x) \bigvee Q(x, f(x))\end{displaymath}


\begin{displaymath}P(z) \bigvee \neg Q(z,w)\end{displaymath}


next up previous
Next: About this document ... Up: predCalc Previous: Predicate Calculus Example (p.
Randy Latimer 2000-12-21