LARA

This is an old revision of the document!

Ground Terms as Domain of Interpretation

Recall syntax of first-order logic terms in First-Order Logic Syntax.

Ground term is a term $t$ without variables, i.e. $FV(t)=\emptyset$, i.e. given by grammar: \[ 

  GT ::= f(GT,\ldots,GT)

\] i.e. built from constants using function symbols.

Example

If ${\cal L}$ has no constants then $GT$ is empty. In that case, we add a fresh constant $a_0$ into the language and consider ${\cal L} \cup \{a_0\}$ that has a non-empty $GT$. We call the set $GT$ Herbrand Universe.

Goal: show that if a formula without equality (for now) has a model, then it has a model whose domain is Herbrand universe, that is, a model of the form $I_H = (HU,\alpha_H)$.

How to define $\alpha_H$?

Term Algebra Interpretation for Function Symbols

Let $ar(f)=n$. Then $f : GT^n \to GT$

$\alpha_H(f)(t_1,\ldots,t_n) =$

This defines $\alpha_H(f)$. How to define $\alpha_H(R)$ to ensure that elements of a set are true, i.e. that $e_S(S)(I_H) = {\it true}$?

  • is this possible for arbitrary set?

Example

Ground Atoms

If $R \in {\cal L}$, $ar(R)=n$ and $t_1,\ldots,t_n \in GT$, we call $R(t_1,\ldots,t_n)$ an Herbrand Atom. HA is the set of all Herbrand atoms: \[ 

  HA = \{ R(t_1,\ldots,t_n) \mid R \in {\cal L}\ \land \ t_1,\ldots,t_n \in GT \}

\]

We order elements of $HA$ in sequence (e.g. sorted by length) and establish a bijection $p$ with propositional variables \[ 

 p : HA \to V

\] We will write $p(A)$.

Example

Expansion of a Clause

Recall that we do not write quantifiers in the clause, but when we say that a clause is true in a model we mean that its universal closure is true.

We obtain an instance of a clause $C$ by replacing all variables with some ground terms from $GT$.

Define \[ 

 expand(C) = \{ subst(\{x_1 \mapsto t_1,\ldots,x_n \mapsto t_n\})(C) \mid FV(C) = \{x_1,\ldots,x_n\}\ \land\ t_1,\ldots,t_n \in GT \}

\]

Note that if $C$ is true in $I$, then $expand(C)$ is also true in $I$ ($expand(C)$ is a consequence of $C$).

We expand entire set: \[ 

 expand(S) = \bigcup_{C \in S} expand(C)

\]

Clauses in the expansion have no variables, they are ground clauses.

Constructing a Propositional Model

We can view the set $expand(S)$ as a set of propositional variables with “long names”.

For an expansion of clause $C_G$ we can construct the corresponding propositional formula $p(C_G)$.

Example

Define propositional model $I_P : V \to \{{\it true},{\it false\}\}$ by \[ 

  I_P(p(C_G)) = e_F(C_G)(I)

\]

Let \[ 

 propExpand(S) = \{ p(C_G) \mid C_G \in expand(S) \}

\]

Lemma: If $I$ is a model of $S$, then $I_P$ is a model of $propExpand(S)$.

Instead of searching for a model, we can search for a propositional model.

If we prove there is no propositional model for $propExpand(S)$, then there is no model for $I$.

What if there is a model $propExpand(S)$? Could it still be the case that $S$ is unsatisfiable?

Constructing Herbrand Model

For $I = (HU,\alpha_H)$ we define $\alpha_H(R)$ so that $I_H$ evaluates ground formulas $expand(S)$ same as in $I_P$ (and thus same as in $I$).

We ensure that atomic formulas evaluate the same:

$ \alpha_H(R) = \{ (t_1,\ldots,t_n)\ \mid $

How does it evaluate non-ground formulas?

Lemma: If $I_P$ is a model for $propExpand(S)$, then $(HU,\alpha_H)$ is a model for $S$.

Herbrand's Theorem

Theorem: The following statements are equivalent:

  • set $S$ has a model
  • set $propExpand(S)$ has a propositional model
  • set $S$ has a model with domain $HU$