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.
Need Help
Hi,
I dont understand the first step in the transformation to CNF for resolution calculus on excercise 9.2 (assignments):
-see screenshot in attachment !-
How can I remove the v here? Or how can i use vF?
Ty for your help:)
Attachment:
cnf.PNG: https://fsi.cs.fau.de/unb-attachments/post_163363/cnf.PNG
Just do it the Gloin way / Freestyle. I hope that’s allowed in the exam, I think it is since the prof cares more about concepts than syntax
A CNF means big AND outside and OR’s inside the clause.
So …; …; …; actually means … and … and …
And if you want to NOT have A or B or C then you need to have NOT A AAAAND NOT B AAAAAND NOT C.
Also OR is associative (That means you can remove and add brackets as you wish. Like you can do X + Y + Z = (X + Y) + Z in Math. That’s why you get those two single literals)
Does this help?
Yes thank you !
I think i will do it the gloin way and hope it doenst matter which “style” we use, if the result of the CNF is the same in the end.
I just got confused with the upper big F/T f.e. (P v Q)F…
You think we can use the negate sign “¬” ? → ¬(P v Q)
I think not if we’re asked to use this CNF calculus. But that would be pretty annoying thing to ask. I really hope that we don’t need to annotate all those stupid rules we’ll forget after the exam anyway…
If you want to do everything “by the book”, recall that the first order CNF-transformation calculus also contains all of the rules from the propositional calculus. These are being applied here. Check slides 329-331 for the details.