Neha Patil (Editor)

Herbrand structure

Updated on
Edit
Like
Comment
Share on FacebookTweet on TwitterShare on LinkedInShare on Reddit

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

Contents

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

Definition

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 formula 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

    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

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

    Definition

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

    1. U = T0
    2. fS(t1, ..., tn) = f(t1, ..., tn) for every n-ary function symbol f ∈ σ and t1, ..., tn ∈ T0
    3. cS = c for every constant c ∈ σ

    Remarks

    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

    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

    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

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

    Examples

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

    References

    Herbrand structure Wikipedia
    (Text) CC BY-SA