Lab for Automated Reasoning and Analysis LARA

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