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 ◻
.
Formula  Clausal Form 

A

{{A}}

A ∨ ¬A

{{A, ~A}}

A ∧ (B ∨ ¬C) ∧ D

{{A}, {B, ~C}, {D}}

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
true
or false
.
The procedure pl_simplify1(F, S)
outputs S
which is a rewriting of F
where
unnecessary connectives are removed.
The procedure 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.
The procedure 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.
Note that 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 ord_union/3
.
Note that 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 entrypoint for clausal form creation couldn't be simpler.
pl_clausal_form(A, Result) :
pl_simplify(A, SimplifiedA),
pl_clausal_form_conjunction(SimplifiedA, Result).
Chang, CL, Lee, R CT. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
Doets, Kees. From Logic to Logic Programming. MIT Press, 1994.
Fitting, Melvin. FirstOrder 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.