Programming Lab 2: Prenex Conjunctive Normal Form

Submission deadline: Wednesday, May 11, 2016 (11:59 p.m.)

TA: Diego Alejandro Montoya-Zapata

Introduction

The aim of this programming assignment is to translate first-order logic (FOL) formulae to the prenex conjunctive normal form (PCNF).

A formula is in PCNF if it is of the form

        Q₁x₁ ... Q_nx_n M

where the Q_i are quantifiers and M is a quantifier-free formula in conjunctive normal form. The (possibly empty) sequence Q₁x₁ ... Q_nx_n is called the prefix and M is called the matrix [Ben-Ari (2012), Definition 9.9 and van Dalen (2013), Definition 3.5.10]. Every formula in FOL can be transformed into an equivalent formula in PCNF [van Dalen (2013), Theorem 3.5.11].

Assignment (80%)

Download the GitHub repository logic-cm0845- lab2.
- The module FOL defines a data type for the formulae in FOL.
- The module Examples gives some examples of the data type Formula.
- The module CNF has implementations of some steps to get the CNF from a formula in predicate logic.
- The module PCNF has some help to solve the programming lab.
(35%) Using the module FOL, define a function
```
          pcnf :: Formula -> Formula
        
```
that returns the PCNF of a given formula in FOL.
You can use the modules CNF and PCNF, although it is not mandatory. If you decide to use these modules, fill in the blanks by replacing the undefined in the module PCNF with code of your own.
(35%) Oral exposition. Answers and explanations given in the revision of the lab.
(10%) Annotate your source code in a way that explains your solution for the assignment. Improve it with HLint.

Clean code (10%)

Before submitting your code, clean it up! Clean code:

Does not have long lines (at most 80 columns).
Has a consistent layout.
Has type signatures for everything.
Has good comments.
Has no junk (unused code, commented code, unnecessary code).
Has no overly complicated function definitions.
Does not contain any repetitive code.
Has no unnecessary spaces at the end of a line, or empty lines at the end of a file (see: Fixing trailing whitespace issues with Emacs).

Submission (10%)

Submission is electronic. Send an email to asr(at)eafit(dot)edu(dot)co and dmonto39(at)eafit(dot)edu(dot)co and attach a compressed file (.zip or .tar.gz) with your solution.

Your submission has to include the following:

PCNF.hs, a Haskell module file with your solution for the assignment.
README.txt (or README.md), a file containing at least the following information:
- The name of your program.
- Your name.
- A general description of your program.
- Information on how to use your program.

Notes

The programming lab is individual.
You are to use the Haskell Platform ≥ 7.10.2-a or GHC ≥ 7.10.2.
You can add class constraints to the type signature of pcnf if you need them.

Bibliography

Ben-Ari, Mordechai (2012). Mathematical Logic for Computer Science. 3rd ed. Springer.

van Dalen, Dirk (2013). Logic and Structure. 5th ed. Springer.

CM0845 Logic