Did you know ... | Search Documentation: |
![]() | Pack narsese -- jmc/parameterize.md |
Parameterizing Models of Propositional
Calculus Formulas
John McCarthy
Computer Science Department
Stanford University
jmc@cs.stanford.edu
http://www-formal.stanford.edu/jmc/
December 24, 2003
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 p1, . . . , pn is called satisfiable if it
has a model, i.e. a tuple of truth values for p1, . . . , pn 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 p1, . . . , pn of
the formula π as propositional expressions in other variables r1, . . . , rk, such
that arbitrary values of r1, . . . , rk give rise to exactly the values of p1, . . . , pn
satisfying π.
Here are some examples.
p2 = true.
• π = p1p2. this is a trivial case and the formulas are p1 = true and
• π = p1 ≡ p2. We have p1 = r1 and p2 = r1.
• π = p1 ∨ p2. We have p1 = r1 and p2 = ¯r1 ∨ ¯r2.
• π = true. We have p1 = r1 and p2 = r2.
• π = false. No model.
The number of parameters required depends on the number N of models
of π. Indeed it is ceiling(log2(N ))
, the least it could possibly be. Here’s how
to construct a parametrization.
Let π be written in disjunctive normal form. Choose enough variables
r1, . . . , rk, so that each conjunction is assigned one or more of the 2k con-
junctions of the ri and ¯ri. The assignment can be arbitrary provided each
conjunction of the pis gets a unique conjunction of the rjs. For each pi, we
write a conditional expression
if case 1 then tv 1
else if case 2 then tv 2
...
else if case 2k then tv 2k ,
(1)
where the cases are the r-conjunctions and the tv ’s are the truth values
that pi 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
π = (p1p2p3) ∨ (¯p1p2 ¯p3) ∨ (p1 ¯p2p3).
(2)
We need only 2 r 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
p1 = if r1r2 then t else if r1¯r2 then t else if ¯r1r2 then f else if ¯r1¯r2 then tp2 = if r1r2 then t else if r1¯r2 then t else if ¯r1r2 then t else if ¯r1¯r2 then fp3 = if r1r2 then t else if r1¯r2 then t else if ¯r1r2 then f else if ¯r1¯r2 then tRemarks:
optimal in the number of r-variables.
putting the theory in disjunctive normal form leads to an excessively
long expression, the parametrization may be more difficult.
This will depend on the modal logic.
for a group is the problem of group classification with its hundred year
history. However, Abelian groups are nicely parameterized.
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.