LARA

Differences

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

Link to this comparison view

Next revision Both sides next revision
sav07_lecture_8 [2007/04/06 14:22]
vkuncak created
sav07_lecture_8 [2007/04/06 14:23]
vkuncak
Line 14: Line 14:
  
   * the idea of Fourier-Motzkin elimination   * the idea of Fourier-Motzkin elimination
 +
  
 ==== Resolution through an example ==== ==== Resolution through an example ====
 +
 +  (ALL x. EX y. R(x,​y)) ​ &
 +  (ALL x y z. R(x,y) --> R(x, plus(x,​z))) ​ &
 +  (Ev(x) | Ev(plus(x,​1))) -->
 +    (ALL x. EX y. R(x,y) & E(y))
  
 Review of transformation to clauses, unification and resolution rule. Review of transformation to clauses, unification and resolution rule.