This is an old revision of the document!
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
- the idea of Fourier-Motzkin elimination
Resolution through an example
Review of transformation to clauses, unification and resolution rule.
The meaning of completeness and soundness of resolution.