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

• transformation to conjunctions of literals

• the idea of Fourier-Motzkin elimination

(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.

Galois connection. Characterization of injective and surjective functions. Two equivalent definitions of Galois connection.