LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav07_lecture_8 [2007/04/06 14:23]
vkuncak 		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
 +
 +
  
  
Line 19: Line 26:
  
   (ALL x. EX y. R(x,​y)) ​ &   (ALL x. EX y. R(x,​y)) ​ &
-  (ALL x y z. R(x,y) --> R(x, plus(x,z)))  &+  (ALL x y z. R(x,y) --> R(x, plus(y,z)))  &
   (Ev(x) | Ev(plus(x,​1))) -->   (Ev(x) | Ev(plus(x,​1))) -->
     (ALL x. EX y. R(x,y) & E(y))     (ALL x. EX y. R(x,y) & E(y))
  
-Review of transformation to clauses, unification ​and resolution rule.+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.