next up previous
Next: Friday, January 28 Up: Lecture Notes Previous: Tuesday, Jan 25: Lab

Wednesday, January 26

There is an important feature of Boolean algebra as a formal system
which may be so obvious as to be invisible.  We allow ourselves to 
replace any expression with an equivalent expression in the course of
a calculation (and we also allow uniform replacement of any letter in
a theorem with the same expression to generate a new theorem).  These are
the familiar rules of algebraic calculation familiar from high school
in a new context.

We present these rules in some detail.  Let A[B/X] represent the
propositional formula which results when we replace the propositional
letter (variable) X with the propositional formula B in the
propositional formula A.  We have the following rules:

1. A == A is a theorem for any formula A. (equivalence is reflexive).

2. if A == B is a theorem then B == A is a theorem.  (equivalence is
symmetric).

3.  if A == B and B == C are theorems, then A == C is a
theorem.  (equivalence is transitive).  

4.  if B == C is a theorem, then A[B/X] == A[C/X] is a
theorem. (equals can be substituted for equals).

5.  if A == B is a theorem, then A[C/X] == B[C/X] is a theorem.  (any
more specific value can replace a variable everywhere in an
equation).

These are the basic rules of inference used in algebra, except that we
have equivalence instead of equality.  There is an important difference
between axioms (statements we agree are true when we start developing
a logical or mathematical theory) and rules of inference (procedures
which we accept for deriving new true statements (theorems) from old).

To see how these principles work in algebraic reasoning (and even
how they might be formalized in theorem proving or computer algebra
software) let's take a look at what happens when an algebraic rule is
applied in the example we did on Tuesday.

Here's some text from the Tuesday notes:

The result is

== ((~P | Q) | ((~R | S) & (~S | R))) & ((~Q | P) | ((~R | S) & (~S | R)))

We then distribute on the right in the left conjunct to get

== (((~P | Q) | (~R | S)) & ((~P | Q) | (~S | R))) &

	((~Q | P) | ((~R | S) & (~S | R)))

We are given the equation A | (B & C) == (A|B) & (A|C).

We can use property 5 to conclude that

(~P | Q) | ((~R | S) & (~S | R)) == 
((~P | Q) | (~R | S)) & ((~P | Q) | (~S | R))

(actually, we use property 5 three times, once replacing A with (~P | Q),
once replacing B with (~R | S), and once replacing C with (~S | R)).

We then use property 4 to prove the main result:

consider the term X & ((~Q | P) | ((~R | S) & (~S | R))), and replace
X by (~P | Q) | ((~R | S) & (~S | R)) to get the left side of the desired
equation and by ((~P | Q) | (~R | S)) & ((~P | Q) | (~S | R)) to get
the right side of the equation.

All of this might seem obvious and tedious when put this way.  It's the
same as what you might do in showing an algebraic step like this:

(a+b)(c+d) - u(v+w) =

(a(c+d) + b(c+d)) - u(v+w)

The logical analysis of this calculation would look much the same.  This
calculation is easy and obvious for all of you because it's familiar
from high school algebra; I want to make the point that generalizing those
algebra skills (and understanding how to generalize them) will allow
you to do computations in more general contexts.

There's another analysis of this calculation which might be instructive.
We'll look at how a computer program like Watson determines that the
distributive law we used in the previous example can be applied
and carries out the application.

We are trying to apply the distributive law A|(B&C) == (A|B)&(A|C)
to the term (~P | Q) | ((~R | S) & (~S | R)).

The verification that the law applies proceeds by a process of
``matching'' the structure of the parse trees of the term A|(B&C) and
the term (~P | Q) | ((~R | S) & (~S | R)).

        |                             |
        :                             :
        :                  --------------------------
  -------------            :                        :
  :           :            |                        &
  A           &         -------             -----------------
         -----------    :     :             :               :
         :         :    ~     Q         ---------     -------------
         B         C    :               :       :     :           :
                        P               ~       S     ~           R
                                        :             :
                                        R             S


The story goes as follows: at the top level, both terms match (we see
that | is the top-level connective in both cases.  So we match the
corresponding subterms.  On the left, the variable A matches the term ~P|Q,
so we record something like A --> ~P|Q.  On the right, we see terms which
match so far (they are both conjunctions) so we match their corresponding
subterms.  On the left, we have B matching ~R|S, so we record B --> ~R|S.
On the right, we have C matching ~S|R, so we record C --> ~S|R.

We use the list of variable matchings we have constructed:

A --> ~P|Q
B --> ~R|S
C --> ~S|R                                    

as a directive to make substitutions in the other side (A|C) & (A|B)
of the equation we are applying:

the result is 

((~P | Q) | (~R | S)) & ((~P | Q) | (~S | R))

The rules of the matching process are that at each step we have to see
the same ``top connective'' (and match corresponding subterms) or see
a propositional letter (in a more general context, a free variable) matching
any term.  Moreover, the matches assigned to propositional letters must
be consistent.

For example, if we tried to use the same procedure to apply the
theorem P&P == P to the formula A&B we would need to match the term
P&P to the term A&B: the first step would succeed (the two terms have
the same top connective) but we would get two different matches

P --> A
P --> B

when we tried to match the subterms, which indicates that the theorem cannot
be applied (the matching process fails).

This is also an outline of the procedure that the theorem prover uses
when it tries to apply a theorem.  I hope that you see that this is a
procedure which lends itself to computer implementation.



Randall Holmes
2000-05-05