# Differences

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

 — sav07_lecture_8_skeleton [2007/04/12 14:15] (current)vkuncak created 2007/04/12 14:15 vkuncak created 2007/04/12 14:15 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.