Tip:
Highlight text to annotate it
X
Propositional resolution works only on expressions in clausal form. Before a
propositional resolution can be applied, our premises and conclusions must be
converted to this form. Fortunately, as we shall see, there is a simple procedure for
making this conversion. A literal is either an atomic sentence or a negation of
an atomic sentence. For example, if p is a logical constant, the sentences shown here
are all literals. A clausal sentence is either a literal or a disjunction of
literals. And a clause is a finite set of literals, interpreted as a disjunction.
The set can contain one element, two elements, or more elements. Note that the
empty set is also a clause. It's equivalent to an empty disjunction, and
therefore is unsatisfiable. Why is that? Well remember that a clause is a
disjunction. The more disjuncts we have in a clause, the easier it is to satisfy. The
fewer disjuncts, the harder it is to satisfy. In the limit, when there are no
disjuncts, we have an unsatisfiable clause. As we shall see the empty clause
is a particularly important special case in resolution. As mentioned earlier,
there's a simple procedure for converting an arbitrary set of propositional logic
sentences to an equivalent set of clauses. The conversion rules are summarized here.
All of the rules within each group should be applied repeatedly until there are no
changes, before moving on to rules in the next group. The purpose of the
transformations in the implications out group is to eliminate all implications and
biconditionals. We rewrite Phi one implies Phi two as not Phi one or Phi two. And we
re-write a bi-conditional as a conjunction of two transformed implications. The
purpose of the transformations and the negations in the group is to move
negations through other operators until they are applied directly to proposition
constants. We drop double negations, We push nots through ands by negating the
conjuncts and changing to ors. And we push nots through ors by negating the disjuncts
and changing to ands. The purpose of the distr ibution rules is to push or
operators to the inside of and operators, and to normalize every disjunction of
disjuncts to a single disjunction And every conjunction of conjunctions to a
single conjunction. The purpose of the final step, operators out, is to turn
disjunctions into clauses, and to turn conjunctions of clauses into separate
clauses. As an example, consider the job of converting the sentence, g and r
implies f, to clausal form. The conversion process is shown here. In the i step, we
eliminate the implication operator. The n step, in this case, has no effect, same
for the d step. In the o step, we change each of the conjuncts to a clause. There's
a slightly more complicated example. Consider the following conversion. We
start with that same sentence except that in this case it's negated. The i step in
this case is the same as before. However, this time around, we have a negation
operator on the outside. And we need to push that in before we can continue. First
we distribute the negation over the conjunction. Then we distributed the
negation over the disjunction in the second conjunct, and then we removed the
double negative. In the d step, we distribute the or operator over the and.
And finally, in the o step, we convert the two conjuncts to clauses. In this case, we
end up with two clauses, each with two literals. Note that even though the
sentences in these two examples are similar to start with, disagreeing on just
that one negation operator, results are quite different. This exercise tests your
ability to convert propositional logic sentences to clausal form.