The Method
Vaughan Pratt
The method represents a theory as the set of its satisfying valuations,
those that make every formula in the theory true. Sets are represented
as in Pascal, namely as bit vectors. There being 16 valuations of four
variables (the default case n = 4), the bit vectors are of length 16,
which in the program are typed as uint (unsigned int). Theories range
from 1 to 65534, with 0 (the inconsistent theory) and 65535 (the
tautology) being omitted.
The theories being finitely generated and therefore finite, they can be
represented as single propositions, namely their conjunction,
equivalently their strongest member. Every theory (including 0 and the
tautology) can be obtained as a Boolean combination of the variables p_0
through p_3, which themselves constitute theories, respectively 0xaaaa,
0xcccc, 0xf0f0, and 0xff00, denoted p[0] through p[3] in the
implementation; as such these realize the generators of a free Boolean
algebra under the usual bitwise Boolean operations. Boolean
combinations of theories can therefore be expressed directly in the
implementation using C's bitwise Boolean operators: x&y for conjunction,
x|y for disjunction, ~x for complement, and x^y for exclusive-or. For n
< 4 (i.e. when running the implementation for fewer than 4 variables),
the unused p_i's are still there in this particular implementation but
are simply not touched.
The method linearly orders the theories via the standard ordering on
uints interpreted as natural numbers. To each theory t is associated
its reduct r[t], namely the (numerically) least theory currently known
to be equivalent to t under interchange of variables and complementation
of literals. Initially r[t] = t for all theories t. Whenever s and t
are determined to be equivalent, they are "joined" by setting both r[s]
and r[t] to min(r[s],r[t]) (by no means the asymptotically fastest
implementation of JOIN, but more than adequate for the present purpose).
The method is repeated until r stabilizes, at which point the answer
is given by the number of t's that still satisfy r[t] = t, these being
the normal-form theories, defined as the numerically least
representatives of their respective equivalence classes.
The method enumerates all consistent nontautological theories t. For
each it considers variables p_i and p_j for 0 <= i < j <= 3 (6 pairs).
It joins t with the theory obtained by complementing p_i, and with the
theory obtained by interchanging p_i and p_j. These two theories are
determined as per the following two paragraphs respectively.
Complementing p_i has the effect of interchanging the set p[i] of
valuations for which p_i = 1, i.e. the theory consisting of (the
consequences of) the proposition p_i, with the complementary theory
~p[i] (strictly speaking, T&~p[i] where T is the tautological theory,
but the extra bits from omitting T do no harm). This exchange
effectively moves the former valuations down, and the latter up, by a
distance of 2^i positions in the list of all 16 valuations. It follows
that the resulting theory is given by the OR of ((t & p[i]) >> (1<