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.