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

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.
  1. implFree :: Prop t -> Prop t
  2. nnf :: Prop t -> Prop t
  3. cnf :: Prop t -> [[Prop t]]
  4. 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.