Clausal Form

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 ◻.

Examples

Transformation Algorithm

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.

Implementation

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 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).
       

References

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.