LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Next revision 		Previous revision
sav07_lecture_8 [2007/04/06 14:22]
vkuncak created 		sav07_lecture_8 [2007/04/12 14:16]
vkuncak
Line 1: Line 1:
 +====== Lecture 8 ======
 +
  
 ==== Substitution theorem ==== ==== Substitution theorem ====
Line 10: Line 12:
   * proof of substitution theorem using structural induction   * proof of substitution theorem using structural induction
   * the case of a quantifier as a justification for the definition of capture-avoiding substitution   * the case of a quantifier as a justification for the definition of capture-avoiding substitution
 +
  
 ==== Quantifier elimination from Homework 2 ==== ==== Quantifier elimination from Homework 2 ====
 +
 +  * transformation to conjunctions of literals
  
   * the idea of Fourier-Motzkin elimination   * the idea of Fourier-Motzkin elimination
 +
 +
 +
  
 ==== Resolution through an example ==== ==== Resolution through an example ====
  
-Review of transformation to clauses, unification ​and resolution rule.+  (ALL x. EX y. R(x,​y)) ​ & 
 +  (ALL x y z. R(x,y) --> R(x, plus(y,​z))) ​ & 
 +  (Ev(x) | Ev(plus(x,​1))) --> 
 +    (ALL x. EX y. R(x,y) & E(y)) 
 + 
 +The intuitive infinite model. 
 +Example finite model where this holds. 
 + 
 +Review of transformation to clauses, unification, resolution rule in this example.
  
 The meaning of completeness and soundness of resolution. The meaning of completeness and soundness of resolution.
 +
 +==== Homework 3 review ====
 +
 +Galois connection.
 +Characterization of injective and surjective functions.
 +Two equivalent definitions of Galois connection.