Herbrand structure

From Wikipedia, the free encyclopedia
  (Redirected from Herbrand model)
Jump to: navigation, search

In First-order logic, a Herbrand structure S is a structure over a vocabulary σ, that is defined solely by the syntactical properties of σ. The idea is to take the symbols of terms as their values, e.g. the denotation of a constant symbol c is just 'c' (the symbol).

Herbrand structures play an important role in the foundations of logic programming.

Herbrand universe[edit]

Definition[edit]

Herbrand universe will serve as the universe in Herbrand structure.

(1) The Herbrand universe of a first order language Lσ, is the set of all ground terms of Lσ. If the language has no constants, then the language is extended by adding an arbitrary new constant.

  • It is enumerable, and infinitely countable if a function symbol of arity greater than 0 exists.
  • In the context of first order languages we also speak simply of the Herbrand universe of the vocabulary σ.

(2) The Herbrand universe of a closed formular in Skolem normal form F, is the set of all terms without variables, that can be constructed using the function symbols and constants of F. If F has no constants, then F is extended by adding an arbitrary new constant.

  • Latter definition is important in the context of computational resolution.

Example[edit]

Let Lσ be a first order language with the vocabulary

  • constant symbols: c
  • function symbols: f(.), g(.)

then the Herbrand universe of Lσ (or σ) is {c, f(c), g(c), f(f(c)), f(g(c)), g(f(c)), g(g(c)), ...}.

Notice, that the relation symbols are not relevant for a Herbrand universe.

Herbrand structure[edit]

A Herbrand structure defines terms on top of a Herbrand universe.

Definition[edit]

Let S be a structure, with vocabulary σ, universe U, and a set of all terms T with the subset of all variable free terms T0. S is said to be a Herbrand structure iff

  1. U = T0
  2. for every n-ary f ∈ σ and t1, ..., tnTS it is f σ = f t1, ..., tn
  3. for every c ∈ σ it is cσ = c

Remarks[edit]

  1. U is the Herbrand universe of σ.
  2. A Herbrand structure that is a model of a theory T, is called the Herbrand model of T.

Examples[edit]

For a constant symbol c and a 1-ary function symbol f(.) we have the following interpretation:

  • U = { c, fc, ffc, fffc, ...}
  • fc -> fc, ffc -> ffc, ...
  • c -> c

Herbrand base[edit]

In addition to the universe, defined in Herbrand universe, and the term denotations, defined in Herbrand structure, the Herbrand base completes the interpretation by denoting the relation symbols.

Definition[edit]

A Herbrand base is the set of all ground atoms of whose argument terms are the Herbrand universe.

Examples[edit]

For a 2-ary relation symbol R, we get with the terms from above:

{ R(c, c), R(fc, c), R(c, fc), R(fc, fc), R(ffc, c), ...}

See also[edit]

References[edit]