Any propositional formulae has an equivalent disjunctive normal form
and an equivalent conjunctive normal form.
Definition 2: A disjunctive normal form of a Boolean function is a developed disjunctive normal form is any variable appears once and only once in any clause, either in negative form or not (never under both forms) ;
It is observed that the transformation from a disjunctive normal form to a developed disjunctive normal form is done very easily by replacing clause 0 from the disjunctive normal form that does not contain a key [k.sub.j] with ([empty][conjuction][k.sub.j])[disjunction]([empty][conjuction][bar.[k.sub.j]]).
We search for the correspondence between each term of the disjunctive normal form and generated atoms [C.sub.i].
A classically valid sequent of truth-functional logic is expressible as a sequent with a formula in conjunctive normal form as premise and one in disjunctive normal form
as conclusion, thus (ibid.):
A suitable canonical form is the disjunctive normal form without nonessential variables mentioned before with the additional condition that the corresponding multiset of address constants and variables is minimal with respect to the multiset extension of the strict partial ordering
Suitable canonical forms are the well-known disjunctive normal forms without nonessential variables (variables whose value does not matter).
For a language generated by any finite number of propositional variables there is an easy algorithm for obtaining the sentence [Delta]X in disjunctive normal form, given the truth table of a sentence X.
It is not too difficult to show that if X is a non-contradictory sentence in disjunctive normal form, then [Delta]X may be obtained as the result of performing the following simple operation on X: replace by T all [not p.sub.i]' occurring in X.