Definitional Conjunctive Normal Form, like Conjunctive Normal Form (CNF) is a conjunction of disjunctions of literals. The main advantage of the definitional variant of CNF is that the transformation doesn't give an exponential increase in formula size in the worst case. However, unlike CNF, the transformation is not guaranteed to produce an equivalent form. Instead it produces an equisatisfiable form, that is to say, the transformation is satisfiable if and only if the original is satisfiable. For many cases this is sufficient.
The key idea with this transformation is that we can replace a subformula with a new variable which is equivalent to
this formula. For example, given a ∧ b ∧ c we define p1 to be the subformula a ∧ b giving:
(p1 ⇔ a ∧ b) ∧ p1 ∧ c
We can then proceed with defining p2 to be p1 ∧ c which gives:
(p2 ⇔ p1 ∧ c) ∧ (p1 ⇔ a ∧ b) ∧ p2
The connective ⇔ is equivalent to a conjunction of two disjunctions of two subformulas.
Therefore, a final transformation into CNF shouldn't lead to an exponential increase in formula size
that is possible with the CNF transformation procedure.
Here we show three types of definitional CNF
The algorithm used is taken from Harrison. All three versions of definitional CNF follow the same similar pattern.
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
We also make use of the code given in the definitions of Conjunctive Normal Form
(cnf_transform/2) and
Negation Equivalence Normal Form (nenf_transform/2).
The predicate call pl_make_prop_variable(Id, Number, NewVariable, NewNumber)
succeeds if NewVariable has the name which is the concatenation of the names of
Id and Number, in that order, and NewNumber is Number+1.
We use this to create new propositional variables for our definitions.
pl_make_prop_variable(Id, Number, NewVariable, NewNumber) :-
name(Number, NumberCodes),
name(Id, IdCodes),
append(IdCodes, [0'_|NumberCodes], NewVariableCodes),
name(NewVariable, NewVariableCodes),
NewNumber is Number+1.
The predicate call pl_max_varindex(PrefixAtom, N, Var, Max)
succeeds if Max is the maximum of N and M where M is the number represented by the codes
found in the name of Var after the codes of PrefixAtom.
This is used when we walk the input formula looking for the highest index of the prefix we are going to use for the
propositional variable names for our definitions.
We do this to we avoid variable name clashes.
pl_max_varindex(PrefixAtom, N, Var, Max) :-
name(PrefixAtom, PrefixAtomName),
name(Var, VarName),
( append(PrefixAtomName, VarPostfix, VarName), name(VarNumber, VarPostfix), number(VarNumber) ->
max(N, VarNumber, Max)
; Max = N
).
The predicate call pl_formula_max_varindex(F, P, I, O) succeeds if the maximum index of variables with prefix
P in formula F is O. Here I is the initial index, usually 0.
pl_formula_max_varindex(Atom, Prefix, In, Out) :-
atom(Atom),
!,
pl_max_varindex(Prefix, In, Atom, Out).
pl_formula_max_varindex(~Phi, Prefix, In, Out) :-
pl_formula_max_varindex(Phi, Prefix, In, Out).
pl_formula_max_varindex(Phi /\ Psi, Prefix, In, Out) :-
pl_formula_max_varindex(Phi, Prefix, In, Mid),
pl_formula_max_varindex(Psi, Prefix, Mid, Out).
pl_formula_max_varindex(Phi \/ Psi, Prefix, In, Out) :-
pl_formula_max_varindex(Phi, Prefix, In, Mid),
pl_formula_max_varindex(Psi, Prefix, Mid, Out).
pl_formula_max_varindex(Phi => Psi, Prefix, In, Out) :-
pl_formula_max_varindex(Phi, Prefix, In, Mid),
pl_formula_max_varindex(Psi, Prefix, Mid, Out).
pl_formula_max_varindex(Phi <=> Psi, Prefix, In, Out) :-
pl_formula_max_varindex(Phi, Prefix, In, Mid),
pl_formula_max_varindex(Psi, Prefix, Mid, Out).
The predicate call pl_definitional_cnf_map_cnf(F, Acc, Result) creates the CNF for each member of the list of input
formulas F and conjoins them altogether to create Result.
The argument Acc is the accumulation of the CNF conjunction as we progress through the input.
The CNF transformation is an expensive operation so doing it conjunct by conjunct
is easier than just conjoining them all and calling cnf_transform/2 once.
pl_definitional_cnf_map_cnf([], Conjuncts, Conjuncts).
pl_definitional_cnf_map_cnf([Phi|Phis], Acc, Conjuncts) :-
cnf_transform(Phi, Conjunct),
pl_definitional_cnf_map_cnf(Phis, Conjunct /\ Acc, Conjuncts).
The predicate call pl_definitional_cnf(Phi, Din, Nin, Psi, Dout, Nout)
is used to build a definition.
If Phi is a compound (not atomic) NENF formula, Din a set of variable-definition pairs, and
Nin the maximum var index in Phi, then Psi is a variable with index Nin+1,
Dout is the updated set of variable-definition pairs, and Nout is the updated max index.
Otherwise Ps=Phi, Din=Dout, Nin=Nout.
pl_definitional_cnf(FormIn, Defns, N, FormOut, Defns4, N4) :-
compound(FormIn),
FormIn =.. [Op, Phi, Psi],
!,
member(Op, [(\/), (/\), (<=>)]),
NewForm =.. [Op, Phi2, Psi2],
pl_definitional_cnf(Phi, Defns, N, Phi2, Defns2, N2),
pl_definitional_cnf(Psi, Defns2, N2, Psi2, Defns3, N3),
( member(Var-NewForm, Defns) ->
FormOut = Var,
Defns4 = Defns3,
N3 = N4
;
pl_make_prop_variable('p', N3, NewVar, N4),
FormOut = NewVar,
Defns4 = [NewVar-NewForm|Defns3]
).
pl_definitional_cnf(Phi, Defns, N, Phi, Defns, N).
The predicate call pl_definitional_cnf(Phi, Psi)
transforms Psi into the definitional CNF Phi.
pl_definitional_cnf(PhiIn, PhiOut) :-
pl_formula_max_varindex(PhiIn, 'p', 0, N),
M is N+1,
nenf_transform(PhiIn, PhiNENF),
pl_definitional_cnf(PhiNENF, [], M, PhiDef, Defns, _),
findall((A<=>B), member(A-B, Defns), Lst),
pl_definitional_cnf_map_cnf(Lst, PhiDef, PhiOut).
Note that we can avoid unnecessary computations if the top-level connective is a conjunction. In this case we just treat each conjunct separately then conjoin the results. Also, if any of these conjuncts are disjunctions, we can ignore any atomic disjuncts as they are already in CNF and don't need to part of a definition.
The predicate call pl_and_cnf(Form1, Defns1, N1, Form2, Defns2, N2)
recurses through the iterated conjunctions of Form1 with Defns1 and N1.
Defns1 are the definitions created so far and N1 is the next index to be used for a
definition variable.
The conjuncts are passed onto pl_or_cnf/6.
The resulting definitions are DefnsOut and the last index used for a definition variable is N2-1.
pl_and_cnf(Phi /\ Psi, Defns, N, PhiOut /\ PsiOut, DefnsOut, Nout) :-
pl_and_cnf(Phi, Defns,N, PhiOut, DefnsMid, Nmid),
pl_and_cnf(Psi, DefnsMid, Nmid, PsiOut, DefnsOut, Nout).
pl_and_cnf(Form, Denfs, N, FormOut, DefnsOut, Nout) :-
pl_or_cnf(Form, Denfs, N, FormOut, DefnsOut, Nout).
The predicate call pl_or_cnf(Form1, Defns1, N1, Form2, Defns2, N2)
recurses through the iterated disjunctions of Form1 with Defns1 and N1.
Defns1 are the definitions created so far and N1 is the next index to be used for a
definition variable.
The disjuncts are passed onto pl_definitional_cnf/6.
The resulting definitions are DefnsOut and the last index used for a definition variable is N2-1.
pl_or_cnf(Phi \/ Psi, Defns, N, PhiOut \/ PsiOut, DefnsOut, Nout) :-
pl_or_cnf(Phi, Defns,N, PhiOut, DefnsMid, Nmid),
pl_or_cnf(Psi, DefnsMid, Nmid, PsiOut, DefnsOut, Nout).
pl_or_cnf(Form, Denfs, N, FormOut, DefnsOut, Nout) :-
pl_definitional_cnf(Form, Denfs, N, FormOut, DefnsOut, Nout).
The predicate call pl_optimised_definitional_cnf(Phi, Psi)
transforms Psi into the optimised definitional CNF Phi.
pl_optimised_definitional_cnf(PhiIn, PhiOut) :-
pl_formula_max_varindex(PhiIn, 'p', 0, N),
M is N+1,
nenf_transform(PhiIn, PhiNENF),
pl_and_cnf(PhiNENF, [], M, PhiDef, Defns, _),
findall((A<=>B), member(A-B, Defns), Lst),
pl_definitional_cnf_map_cnf(Lst, PhiDef, PhiOut).
The non-optimised definitional CNF transformation resulted in 3-CNF, that is
each conjunct is a disjunct of at most 3 literals. This isn't the case
with the optimised definitional CNF. A simple solution is to just
treat each conjunct separately and pass the conjuncts to the definitional
CNF transformation routine. Basically, this is the optimised definitional
CNF that skips the pl_or_cnf/6 call.
The predicate call pl_and_cnf3(Form1, Defns1, N1, Form2, Defns2, N2)
recurses through the iterated conjunctions of Form1 with Defns1 and N1.
Defns1 are the definitions created so far and N1 is the next index to be used for a
definition variable.
The conjuncts are passed onto pl_definitional_cnf/6.
The resulting definitions are DefnsOut and the last index used for a definition variable is N2-1.
pl_and_cnf3(Phi /\ Psi, Defns, N, PhiOut /\ PsiOut, DefnsOut, Nout) :-
pl_and_cnf3(Phi, Defns,N, PhiOut, DefnsMid, Nmid),
pl_and_cnf3(Psi, DefnsMid, Nmid, PsiOut, DefnsOut, Nout).
pl_and_cnf3(Form, Denfs, N, FormOut, DefnsOut, Nout) :-
pl_definitional_cnf(Form, Denfs, N, FormOut, DefnsOut, Nout).
The predicate call pl_optimised_definitional_cnf3(Phi, Psi)
transforms the formula Phi into the definitional 3-CNF Psi.
pl_optimised_definitional_cnf3(PhiIn, PhiOut) :-
pl_formula_max_varindex(PhiIn, 'p', 0, N),
M is N+1,
nenf_transform(PhiIn, PhiNENF),
pl_and_cnf3(PhiNENF, [], M, PhiDef, Defns, _),
findall((A<=>B), member(A-B, Defns), Lst),
pl_definitional_cnf_map_cnf(Lst, PhiDef, PhiOut).
Harrison, John. Handbook of Practical Logic and Automated Reasoning. Cambridge, 2009.
Copyright © 2014 Barry Watson. All rights reserved.