LARA

Herbrand Model and Unsat Proof for an Example

Herbrand

We will look at the language ${\cal L} = \{P, R, a, f\}$ where

  • $P$ is relation symbol of arity one
  • $R$ is relation symbol of arity two
  • $a$ is a constant
  • $f$ is a function symbol of two arguments

Consider this formula in ${\cal L}$:

\begin{equation*}
\begin{array}{l@{}l}
  & (\forall x. \exists y.\ R(x,y))\ \land \\
      & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\ \land \\
      & (\forall x.\ P(x) \lor P(f(x,a)))\ \\
      & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y)
\end{array}
\end{equation*}

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):

\begin{equation*}
\begin{array}{l@{}l}
\lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\
      & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\ \land \\
      & (\forall x.\ P(x) \lor P(f(x,a)))\ \big)\\
      & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg)
\end{array}
\end{equation*}

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.