I'm taking a basic intro to logic course in Computer Science, and there's a topic that's baffling me. The instructor seems to be of not much help, and the study group I'm in doesn't seem to fully understand either. Maybe somebody here can help understand what this is?
I know what Resolution is, and how to do it for very simple cases... but there's a method to reduce an expression to something usable in CNF form. Problem is, the notes that we're given don't seem to explain it very well. Does anybody know what this process is called, and if there's better examples of how it works online somewhere?
Here's the part of our notes: