Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
CNF1 Algorithm in Problems 11.2 and 11.3
In these problems you are asked to apply the resolution calculus for first order logic. However, you do not have to strictly apply the CNF1 algorithm to get the formulae into CNF. Instead you are allowed to do it as in the attached slide.
Attachment:
negatefirst.PNG: https://fsi.cs.fau.de/unb-attachments/post_163196/negatefirst.PNG
If this procedure gives you a stomach-ache, console yourself by recalling that the existential quantifier is merely an abbreviation. So when you are “dragging” the negation inside you are not changing anything in the abbreviation-free version of the formula.