Required reading for Wednesday

Folks
 
 Please read the following parts from the text for Wednesday's class. We will likely do just one class on FOPC inference and so it will help if you have read this stuff before.

9.1. Propositional vs. First-Order Inference ... 272
       Inference rules for quantifiers ... 273
       Reduction to propositional inference ... 274
9.2. Unification and Lifting ... 275
       A first-order inference rule ... 275
       Unification ... 276
      
9.4. Backward Chaining ... 287
       A backward chaining algorithm ... 287

9.5. Resolution ... 295
       Conjunctive normal form for first-order logic ... 295
       The resolution inference rule ... 297
       Example proofs ... 297 
 
       Resolution strategies ... 304
              Unit preference ... 305
              Set of support ... 305
              Input resolution ... 305
              Subsumption ... 306