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