Next: About this document ...
Parameterizing Models of Propositional Calculus Formulas
John McCarthy
Computer Science Department
December 24, 2003
Stanford University
Abstract:
It is often inadequate that a theory be consistent, i.e. have
models. It should have enough models. We discuss parameterizing
the set of models in the special case of propositional
satisfiability.
A propositional formula in variables
is called satisfiable if it has
a model, i.e. a tuple of truth values for
that makes true. Many programs exist for deciding this.
However, we can ask for more than just whether a formula has models;
we can ask about its set of models. One way to get a grip on the set
of a formula's models is to parametrize it, i.e. to express the
variables
of the formula as propositional
expressions in other variables
, such that arbitrary
values of
give rise to exactly the values of
satisfying .
Here are some examples.
The number of parameters required depends on the number of
models of . Indeed it is
, the
least it could possibly be. Here's how to construct a
parametrization.
Let be written in disjunctive normal form. Choose enough
variables
, so that each conjunction is assigned one
or more of the conjunctions of the and . The
assignment can be arbitrary provided each conjunction of the s
gets a unique conjunction of the s. For each , we write a
conditional expression

(1) 
where the s are the rconjunctions and the
's are the truth values that assumes in
that case. The conditional expressions can be converted
to propositional expressions if desired, since all the consequents are
truth values.
Example:
[We'll use juxtaposition for conjunction to keep the formulas compact.]
Let

(2) 
We need only 2 variables. These give 4 cases. We can assign the
cases to the three terms of (2) arbitrarily, so let's assign tt
and tf to the first conjunction of (2) and ft and ff to the two
remaining conjunctions. We then have
Remarks:
 Presumably the above systematic procedure usually
doesn't give the optimal parametrization in terms of length
of formula, although it is optimal in the number of rvariables.
 The parametrization is easy, because we have assumed that
the theory is represented by an expression in disjunctive
normal form. If putting the theory in disjunctive normal form leads
to an excessively long expression, the parametrization may be more
difficult.
 There is no apparent way of turning a
parameterization of the models of into a
parameterization of the models of .
 Parameterizing models of modal formulas may offer
difficulties, because there will often be an infinity of
models of even rather simple formulas. This will depend on
the modal logic.
 Extending the idea to predicate calculus is likely
to be reasonable only under some restrictions.
Thus parameterizing the models of the axioms for a group is
the problem of group classification with its hundred year
history. However, Abelian groups are nicely parameterized.
 Perhaps monadic predicate calculus will be a good
domain.
 Parameterizing the models of nonmonotonic theories may
present interesting problems even in the propositional case.
2001 August.
 There may be straightforward ways of going from a
parameterization of a theory to parameterizations of some
kinds of elaborations of the theory. This may help with the
problem of establishing consistency of the elaborated theory.
Thus the mere fact of consistency of a theory may not help in
establishing the consistency of an elaborated theory, but a
parameterization of the theory may lead to consistency of the
elaborated theory via its parameterization.  2001 August.
Next: About this document ...
John McCarthy
20031224