predicate logic in clause form
can somebody tell me how to convert a formula to its corresponding clause form step by stepi?
$¬(∀x∃y P(x,y) → (∀y∃z ¬Q(x,z)∧∀y¬∀z R(y,z))$
i know the formua has to be transformed into cnf fisrt im a bit confused on the first step which is to transform the original formula to rectified form. my teacher told me the only thing i have to do is to check if there is any same variable with quantifiers. then rename it. is it true? can somebody answer the above question step by step so i can watch and learn??
$\endgroup$ 21 Answer
$\begingroup$See Mordechai Ben-Ari, Mathematical Logic for Computer Science (3rd ed - 2012), page 174.
In order to get the CNF for a closed formula of f-o logic, we have to :
Step 1: Rename bound variables so that no variable appears in two quantifiers
Step 2: Eliminate all binary Boolean operators other than ∨ and ∧
Step 3: Push negation operators inward, collapsing double negation, until they apply to atomic formulas only.
Step 4: Extract quantifiers from the matrix. Choose an outermost quantifier, that is, a quantifier in the matrix that is not within the scope of another quantifier still in the matrix. Repeat until all quantifiers appear in the prefix and the matrix is quantifier-free.
Step 5: Use the distributive laws to transform the matrix into CNF.
Now with your example : rename bound variables :
$\lnot (∀x∃yP(x,y)→(∀v∃u¬Q(v,u)∧∀w¬∀zR(w,z)))$ --- I suppose that $∀y∃z¬Q(x,z)∧...$ is a misprint for $∀x∃z¬Q(x,z)∧...$
remove $\rightarrow$ [we have tu use the equivalence between : $p \rightarrow q$ and $\lnot p \lor q$] :
$\lnot (\lnot ∀x∃yP(x,y) \lor (∀v∃u¬Q(v,u)∧∀w¬∀zR(w,z)))$
push $\lnot$ inwards [we have to use (more than one time) De Morgan laws and the equivalence between $\lnot \forall$ and $\exists \lnot$, etc. and, of course, double negation] :
$∀x∃yP(x,y) \land \lnot ((∀v∃u¬Q(v,u)∧∀w∃z\lnot R(w,z)))$
and again :
$∀x∃yP(x,y) \land (∃v∀uQ(v,u) \lor ∃w∀zR(w,z))$
Then we have to move the quantifiers upfront :
$\endgroup$ 24$∀x∃yP(x,y) \land (∃v∀u∃w∀z(Q(v,u) \lor R(w,z))$
$∀x∃y∃v∀u∃w∀z(P(x,y) \land (Q(v,u) \lor R(w,z)))$.
