```November 17

* Resolution

a v ~b, b  =>   c

p1 v p2 v ... v pm,
~p1 v pn v ... v pq,
--------------------
p2 v ... v pm v pn v ... v pq

* Proof by refutation using resolution

To prove a statement using resolution:
1) Convert each statement in database to clausal form
Clausal form is a disjunction of literals
2) Negate the goal statement and convert to clausal form
3) Repeatedly apply resolution to generate new statements
4) If generate empty statement [], proof is complete

Clausal Form is a disjunction of literals
(no quantifiers, no &, no ->, no <->, no parentheses)

Proof by refutation:
We know database statements are all true
Resolution is sound
All statements generated are true if database is true
How can we come up with empty (false) clause?
Only possible false statement is negated goal
If negated goal is false, goal must be true (A v -A is a tautology)

Example
If Linus is sitting in the pumpkin patch, it must be Halloween.
The Great Pumpkin appears on Halloween.
Linus is sitting in the pumpkin patch.
Prove the Great Pumpkin will appear today.

1.  SitPatch(Linus) -> Halloween(Today)
2.  Halloween(Today) -> GrPumpkin(Today)
3.  SitPatch(Linus)
Rewrite:
1.  ~SitPatch(Linus) v Halloween(Today)
2.  ~Halloween(Today) v GrPumpkin(Today)
3.  SitPatch(Linus)
4.  ~GrPumpkin(Today)     ; Negated goal
Proof:
5. ~Halloween(Today)  {2&4}
6. ~SitPatch(Linus)   {1&5}
7. []                 {3&6}
Q.E.D.

Example
If the maid stole the jewelry, then the butler wasn't guilty.
Either the maid stole the jewelry or she milked the cows.
If the maid milked the cows, then the butler got his cream.
Goal:  Therefore, if the butler was guilty, then he got his cream.

G(M) -> ~G(B)
G(M) v Cows(M)
~Cows(M) v Cream(B)
~(G(B) -> Cream(B))
Rewrite:
1. ~G(M) v ~G(B)
2. G(M) v Cows(M)
3. ~Cows(M) v Cream(B)
4. G(B)
5. ~Cream(B)
Proof:
6. ~G(M) {1&4}
7. Cows(M) {2&6}
8. Cream(B) {3&7}
9. [] {5&8}

* Complexity Theory

Until now we put all problems into two categories:  those that can be solved
by algorithms and those that cannot.

Now we realize that some are solvable in principle but not solvable in a
practical sense by computers due to excessive time requirements.

Show computing example.

Suppose your task is to schedule visits of a traveling sales representative
to 10 offices.  You are given a map with the 10 cities and asked to
product itinerary that minimizes total distance traversed.

If there are n cities to visit, the number of possible itineraries to visit
is certainly finite (n-1)!.  One algorithm can examine all itineraries and
compare them to find the shortest.  A TM can be designed to do this.

There are too many tours to be examined in a reasonable amount of time.
For n=10, we have to examine 9! = 362,880 itineraries.
For n=40, we have to examine over 10^45 itineraries.  Even if examine 10^15
tour per second (much more than capable of with today's computers), the
required time would be several billion lifetimes of the universe!

A "practical feasible algorithm" is one that requires only a number of steps
that is a "polynomial" in the size of the input.
Which type of TM do we use?  The choice does not matter.
If one can solve in P time, all can solve in P time (conversions only take
P time).

A TM M is "polynomially bounded" if for an input x, M always halts after at
most p(n) steps, where n is the size of hte input and p is a polynomial
function.

A language is "polynomially decidable" if there is a polynomially bounded TM
that decides it.  The class of all polynomially decidable languages is "P".
```