# Herbrand Model and Unsat Proof for an Example

We will look at the language where

- is relation symbol of arity one
- is relation symbol of arity two
- is a constant
- is a function symbol of two arguments

Consider this formula in :

We are interested in checking the *validity* of this formula (is it true in all interpretations). We will check the *satisfiability* of the negation of this formula (does it have a model):

Parsing the formula.

Negation normal form.

Skolem normal form for each clause.

Herbrand universe.

Propositional expansion.

Propositional proof.

Recovering first-order proof from propositional proof.