# Definitional Conjunctive Normal Form

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

1. (ordinary) definitional CNF.
2. Optimised definitional CNF.
3. Optimised definitional 3-CNF.

## Transformation Algorithm

The algorithm used is taken from Harrison. All three versions of definitional CNF follow the same similar pattern.

1. Calculate the first index of the variable which will be used to define subformulas. The user provides the variable prefix which may be used elsewhere in the input formula so we perform this step to avoid clashes.
2. Transform the formula into Negation Equivalence Normal Form.
3. Create a definition for each subformula following a depth-first search ordering. Definitions are reused, i.e. if we see two identical subformulas then we have only one definition.
4. Form the transformed term using the new definitions.

## 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
``````
``` ```

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

### Ordinary Definitional CNF

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

### Optimised Definitional CNF

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

### Ordinary Definitional 3-CNF

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

## References

Harrison, John. Handbook of Practical Logic and Automated Reasoning. Cambridge, 2009.