Programming Lab 1: Conjunctive Normal Form

TA: Diego Alejandro Montoya Zapata

Introduction

The aim of this programming lab is to translate propositional formulae to the conjunctive normal form.

Syntactical Conventions

The set of well-formed formulae is defined by the following grammar:

      for ::= p         (proposition symbols)
          | ~for        (negation)
          | for ^ for   (conjunction)
          | for ∨ for   (disjunction)
          | for --> for (implication)
          | for <-> for (bi-implication)
    

where ~ has higher precedence than ^, ^ has higher precedence than ∨, ∨ has higher precedence than --> and --> has higher precedence than <->.

Assignment (80%)

A formula is in conjunctive normal form (CNF) if it is a conjunction of disjunctions of literals [Ben-Ari (2012), Definition 4.1]. Every formula in propositional logic can be transformed into an equivalent formula in CNF [Ben-Ari (2012), Theorem 4.3].

• (35%) Write a Prolog program which translate any propositional formulate to CNF. That is, write a Prolog predicate cnf(A,B) where B is the CNF of A.
• (35%) Oral exposition. Answers and explanations given in the revision of the lab.
• (10%) Annotate your source code. Documentation should explain your solution for the assignment.

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 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:

• cnf.pl, a Prolog file with your solution for the assignment.
• README (or README.md), a file containing at least the following information:
  • The name of your program.
  • Your name(s).
  • A general description of your program.
  • The Prolog version used for writing your program.

Notes

The programming lab is individual.

Bibliography

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

CM08451 Logic