- English only

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