The clausal form of a formula in conjunctive normal form (CNF) is a set of sets of literals. Each set of literals is one disjunction of the formula and is this is known as a clause. The set of these clauses represents the conjunction of the formula. Conjunctive normal forms with the same clausal form are equivalent.
The empty clause is often denoted by
We can transform a formula in CNF into a clausal form by a simple syntax directed translation. We simply walk the structure of the formula collecting the disjuncts into clauses, then collecting sets these clauses.
The following code can be found in the examples directory of the Barry's Prolog distribution.
The following Prolog code in this section implements the algorithm given above.
First we fix a set of operators which we will need to represent the formulas of propositional logic.
:-op(200, fy, ~). % Negation
:-op(0, yfx, (/\)).
:-op(400, xfy, (/\)). % Conjunction (not ISO associativity which is yfx)
:-op(0, yfx, (\/)).
:-op(500, xfy, (\/)). % Disjunction (not ISO associativity which is yfx)
:-op(600, xfy, =>). % Implication
:-op(700, xfy, <=>). % Equivalence
To have an easier handling of true and false, we simplify the input CNF by collapsing those disjunctions or conjunctions containing
pl_simplify1(F, S) outputs
S which is a rewriting of
unnecessary connectives are removed.
pl_simplify(F, S) simplifies a formula
F via recursive self application on subterms
followed by a call to
pl_simplify1(F, S) on the resulting form giving result
S. The input is assumed to be in CNF.
pl_simplify1(~true, false) :- !. pl_simplify1(~false, true) :- !. pl_simplify1(~ ~Phi, Phi) :- !. pl_simplify1(_ /\ false, false) :- !. pl_simplify1(false /\ _, false) :- !. pl_simplify1(Phi /\ true, Phi) :- !. pl_simplify1(true /\ Phi, Phi) :- !. pl_simplify1(Phi \/ false, Phi) :- !. pl_simplify1(false \/ Phi, Phi) :- !. pl_simplify1(_ \/ true, true) :- !. pl_simplify1(true \/ _, true) :- !. pl_simplify1(Phi, Phi). pl_simplify(~Phi, S) :- !, pl_simplify(Phi, PhiSimplified), pl_simplify1(~PhiSimplified, S). pl_simplify(Phi /\ Psi, S) :- !, pl_simplify(Phi, PhiSimplified), pl_simplify(Psi, PsiSimplified), pl_simplify1(PhiSimplified /\ PsiSimplified, S). pl_simplify(Phi \/ Psi, S) :- !, pl_simplify(Phi, PhiSimplified), pl_simplify(Psi, PsiSimplified), pl_simplify1(PhiSimplified \/ PsiSimplified, S). pl_simplify(Phi, Phi).
Since a formula in CNF is known to be a conjunction of disjunctions, we first need to recognise a conjunction.
Each conjunct is a disjunction so we pass control to a routine for processing them.
In this implementation we make use of a library which represents sets as ordered lists.
ord_union/3 is from this library.
The result of
pl_clausal_form_disjunction/2 is put into a list to make it a singleton set of a set of literals.
true gives the empty conjunction.
pl_clausal_form_conjunction(A /\ B, Result) :- !, pl_clausal_form_conjunction(A, ResultA), pl_clausal_form_conjunction(B, ResultB), ord_union(ResultA, ResultB, Result). pl_clausal_form_conjunction(true, ) :- !. pl_clausal_form_conjunction(A, [Result]) :- pl_clausal_form_disjunction(A, Result).
The processing of disjunctions is similar to that of conjunctions.
Each disjunct is a literal and we simply create a singleton set for each one.
All disjuncts are collected with
false gives the empty disjunction.
pl_clausal_form_disjunction(A \/ B, Result) :- !, pl_clausal_form_disjunction(A, ResultA), pl_clausal_form_disjunction(B, ResultB), ord_union(ResultA, ResultB, Result). pl_clausal_form_disjunction(false, ) :- !. pl_clausal_form_disjunction(A, [A]).
The entry-point for clausal form creation couldn't be simpler.
pl_clausal_form(A, Result) :- pl_simplify(A, SimplifiedA), pl_clausal_form_conjunction(SimplifiedA, Result).
Chang, C-L, Lee, R C-T. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.
Fitting, Melvin. First-Order Logic and Automated Theorem Proving. Springer, 1990.
Harrison, John. Handbook of Practical Logic and Automated Reasoning. Cambridge, 2009.
Copyright © 2014 Barry Watson. All rights reserved.