CMPS240, Spring 2013, Section 01: Lecture 17 05/30/2013

Know the following for the Final Exam!:

    SAT: Resolution

     Davis-Putnam

     Subtraction

     Walk-Thru Subtraction

      Factoring Subtraction

 

      Proving in First Order Logic:

      Clausification

      Skolemization

      Unification

       Resolution

       EGs.

 

       AxP(x)   in EGs:  (x(P(x))

       ExP(x)   in EGs   xP(x)        (you can only substitute for a variable in an odd contest)!