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.
Recovering first-order proof from propositional proof.