Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav07_lecture_8_skeleton [2007/04/12 14:15] (current)
vkuncak created
Line 1: Line 1:
 +====== Lecture 8 Skeleton ======
 +
 +
 +==== Substitution theorem ====
 +
 +Recall the statement in the optional part of Homework 1.
 +
 +Review of
 +  * semantics of first-order logic
 +  * definition of capture-avoiding substitution and the set of free variables
 +  * structural induction on algebraic data types and comparison to induction on natural numbers
 +  * proof of substitution theorem using structural induction
 +  * the case of a quantifier as a justification for the definition of capture-avoiding substitution
 +
 +
 +==== Quantifier elimination from Homework 2 ====
 +
 +  * transformation to conjunctions of literals
 +
 +  * the idea of Fourier-Motzkin elimination
 +
 +
 +
 +
 +==== Resolution through an example ====
 +
 +  (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.
 +
 +==== Homework 3 review ====
 +
 +Galois connection.
 +Characterization of injective and surjective functions.
 +Two equivalent definitions of Galois connection.
  
 
sav07_lecture_8_skeleton.txt · Last modified: 2007/04/12 14:15 by vkuncak