Problem Set 2: Write a CNF module
Overview
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:
- Learn how Haskell simple Haskell functions as a case analysis over the structure of the input data.
- Learn to write tests along with your code.
- Internalize why some propositions are very expensive
to put in CNF.
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
- Download the stub and edit this file to produce a solution.
- Write the missing functions in the stub.
- implFree :: Prop t -> Prop t
- nnf :: Prop t -> Prop t
- cnf :: Prop t -> [[Prop t]]
- distr :: [[Prop t]] -> [[Prop t]] -> [[Prop t]]
- At the bottom of the file construct at least 3 propositions
appropriate for testing each of the functions above. Run your tests.
You might consider using a testing framework like
HUnit
to organize your tests.
- Write a few additional tests that test the main function toCNF.
- One test should test that in the answer [[Prop a]] every
proposition is a literal (use the literal predicate).
What To Turn In
- Be sure your name is listed as a comment
in your solution, you have named your solution P2.hs
- Drop it in the ProbSet2 folder in the class drop box
- Be prepared to talk about your solution in class.
Back to the class web-page.
Back to the Course Schedule.