Submission deadline: Sunday, March 6, 2016 (11:59 p.m.)
The aim of this programming lab is to translate propositional formulae to the conjunctive normal form.
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 <->.
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].
cnf(A,B) where B is the CNF
of A.Before submitting your code, clean it up! Clean code:
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 programming lab is individual.
Ben-Ari, Mordechai (2012). Mathematical Logic for Computer Science. 3rd ed. Springer.