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".