Recall the statement in the optional part of Homework 1.
- 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.