A doctrine can be seen as a compound proposition —in other words, a formula— whose truth is assumed to hold. A truth assignment that makes this formula true will be said to be consistent with the doctrine.

In dealing with the doctrine, we will make a crucial use of the well-known fact that any formula can be transformed into logically equivalent ones of the form

$$\Phi({\mathcal{D}})\,:=\,\bigwedge_{C\in{\mathcal{D}}}\left(\bigvee_{p\in C}p\right),$$
$$(1)$$
$$(2)$$

where D stands for a collection of subsets of Π . A formula of this form is
called a conjunctive normal form , and the expressions within parentheses
are called its clauses. Generally speaking, a clause means any formula of
the form
$$\phi(C):=\bigvee_{p\in C}p,$$
p, (2)
where C is a subset of Π . Obviously, specifying a clause is equivalent to specifying the associated set C ⊂ Π , and specifying a conjunctive normal form is equivalent to specifying the associated collection D of subsets of Π .

Because of that, in the following we will sometimes refer to the sets C ∈ D themselves as 'clauses' and we may even refer to the collection D as the
'doctrine'.

A conjunctive normal form being true means that each of its clauses is true. On the other hand, a clause being true means that at least one of its literals is true; in other words, if all of its literals but one are known to be false, then the remaining one must be true. Therefore, the doctrine associated with (1) provides the following implications:

$$\begin{array}{r l}{p\,\leftarrow\,\bigwedge_{\begin{array}{l}{\alpha\in C}\\ {\alpha\neq p}\end{array}}\overline{{{\alpha}}},}\end{array}$$
$$\left({\boldsymbol{3}}\right)$$

α, (3)
for any C ∈ D such that p ∈ C . The method developed below will be based crucially on such implications.

The conjunctive normal forms equivalent to a given doctrine are by no means unique. Later on, we will restrict ourselves to the special class of prime conjunctive normal forms, and eventually we will choose a particular member of that class which is known as the Blake canonical form.

These concepts will be introduced in § 4.1.

On the other hand, we adopt from now on the following assumptions:
(D1) The doctrine is satisfiable and it is given in conjunctive normal form.