Problem Set 2: Write a CNF module


In this exercise you will write a function in Haskell that converts propositions into conjunctive normal form. It will operate over the datatype Prop found in the library file Prop.hs.

A formula in conjunctive normal form is a conjunction of disjunctions, where every disjunct is a literal.

A literal is either a propositional letter, or a negated propositional letter. One might write a literal predicate in Haskell as

literal (LetterP x) = True
literal (NotP(LetterP x)) = True
literal other = False

Learning Objectives

As you work through this exercise we expect you to learn the following:

Getting Started

To get started download the solution stub CNF.hs and fill in the blanks by replacing the undefined in the file with code of your own.

The strategy for defining your toCNF function largely follows the implementation outlined in the text on pages 58-63. So if you haven't done so, please read these pages carefully before you begin.

One difference from the strategy in the text is the use of lists of lists of literals for clausal form. In general list of list of literals like [[a,b,c],[e,f]] represents a Prop like AndP (OrP a (OrP b c)) (OrP e f).

What to do

What To Turn In

Back to the class web-page.
Back to the Course Schedule.