Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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:


share|cite|improve this question
up vote 1 down vote accepted

I think the term reducing to normal form is standard. Not sure there is a special name for it.

A better explanation I have found:

  1. Eliminate all operators other than ∧,∨¬
  2. Move all ¬'s inwards by using De Morgan's Laws:
  3. Remove double negations:
  4. Apply distributivity to get conjunction of disjunctions
share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.