Logic for Computer Scientists/Predicate Logic/Herbrand Theories

Herbrand Theories

edit

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 11

edit

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

  • All constants which occur in   are in   (if no constant appears in  , we assume a single constant, say   to be in  ).
  • For every  -ary function symbol   in   and every  ,  .

Examples: Given the clause set  , we construct the Herbrand universe


 


For the clause set   we get the Herbrand universe  .

Definition 12

edit

Let   be a set of clauses. An interpretation   is an Herbrand interpretation iff

  •  
  • For every  -ary function symbol ( )   and  
     

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

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

Definition 13

edit

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   is the set of ground atoms  , where   is a  -ary predicate symbol from   and  


We will notate the assignments of relations to predicate symbols by simply giving a set  , where each element is a literal with its atom is from the Herbrand basis.

Examples:


  •  
  •  
  •  

Definition 14

edit

Let   be an interpretation for a set of clauses  ; the Herbrand interpretation   corresponding to   is a Herbrand interpretation satisfying the following condition: Let   be Elements from the Herbrand universe   for  . By the interpretation   every   is mapped to a  . If  , then   have to be assigned   in  .

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

Lemma 4

edit

If   is a model for a set of clauses, then every corresponding Herbrand interpretation   is a model for  

Theorem 4

edit

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

Proof: If   is unsatisfiable, there is obviously no Herbrand model for  .
Assume that there is no Herbrand model for   and that   is satisfiable. Then, there is a model   for   and according to lemma 4 the corresponding Herbrand interpretation   is a model for  , which is a contradiction.