Logic for Computer Scientists/Predicate Logic/Herbrand Theories

Herbrand TheoriesEdit

Until now we considered arbitrary interpretations of formulae in predicate logics. In particular we sometimes used numbers as interpretation domain and functions, like addition or successor. In the following, we will concentrate on a special case, the Herbrand interpretation and we will discuss their relation to the general case.

Definition 11Edit

Let S be a set of clauses. The Herbrand universe U_H for S is given by:

  • All constants which occur in S are in U_H (if no constant appears in S, we assume a single constant, say a to be in U_H).
  • For every n-ary function symbol f in S and every t_1, \cdots,t_n \in U_H , f(t_1, \cdots , t_n)\in U_H.

Examples: Given the clause set S_1 = \{ P(a),  \lnot P(x) \lor
P(f(x))\}, we construct the Herbrand universe



 U_H = \{ a, f(a), f(f(a)), f(f(f(a))), \cdots \}


For the clause set S_2 = \{ P(x)\lor
Q(x), R(z)\} we get the Herbrand universe U_H =\{a\}.

Definition 12Edit

Let S be a set of clauses. An interpretation \mathcal{I} = (U_\mathcal{I}, A_\mathcal{I}) is an Herbrand interpretation iff

  • U_\mathcal{I} = U_H
  • For every n-ary function symbol (n\geq 0) f and t_1,   \cdots, t_n \in U_H
     f^\mathcal{I} (t_1, \cdots , t_n) =f(t_1,\cdots , t_n)

Note, that there is no restriction on the assignments of relations to predicate symbols (except, that, of course, they have to be relations over the Herbrand universe U_H).

In order to discuss the interpretation of predicate symbols, we need the notion of Herbrand basis.

Definition 13Edit

A ground atom or a ground term is an atom or a term without an occurrence of a variable. The Herbrand basis for a set of clauses S is the set of ground atoms p(t_1, \ldots, t_n), where p is a n-ary predicate symbol from S and t_1, \ldots, t_n \in U_H


We will notate the assignments of relations to predicate symbols by simply giving a set I = \{ m_1, m_2, \cdots , m_n, \cdots \}, where each element is a literal with its atom is from the Herbrand basis.

Examples:


  • S= \{p(x) \lor q(x), r(f(y))\}
  • U_H = \{ a, f(a), f(f(a)), \ldots\}
  • I = \{ p(a), q(a), r(a), p(f(a)), q(f(a)), r(f(a)), \cdots \}

Definition 14Edit

Let \mathcal{I} =( U_\mathcal{I}, A_\mathcal{I} ) be an interpretation for a set of clauses S; the Herbrand interpretation \mathcal{I}^* corresponding to \mathcal{I} is a Herbrand interpretation satisfying the following condition: Let t_1,\ldots, t_n be Elements from the Herbrand universe U_H for S. By the interpretation \mathcal{I} every t_i is mapped to a d_i \in U_\mathcal{I}. If p^\mathcal{I}(d_1, \ldots, d_n) = true (false), then p(t_1,
\ldots, t_n) have to be assigned true (false) in \mathcal{I}^*.

Let us now state a simple, very obvious lemma, which will help us, to focus on Herbrand interpretation in the following.

Lemma 4Edit

If \mathcal{I} is a model for a set of clauses, then every corresponding Herbrand interpretation \mathcal{I}^* is a model for S

Theorem 4Edit

A set of clauses S is unsatisfiable iff there is no Herbrand model for S.

Proof: If S is unsatisfiable, there is obviously no Herbrand model for S.
Assume that there is no Herbrand model for S and that S is satisfiable. Then, there is a model \mathcal{I} for S and according to lemma 4 the corresponding Herbrand interpretation \mathcal{I}^* is a model for S, which is a contradiction.

Last modified on 21 November 2011, at 10:23