Term Algebra - Herbrand Base

The signature σ of a language is a triple consisting of the alphabet of constants O, the function symbols F, and the predicates P. The Herbrand base of a signature σ consists of all ground atoms of σ: of all formulas of the form R(t₁, …, t_n), where t₁, …, t_n are terms containing no variables (i.e. elements of the Herbrand universe) and R is an n-ary relation symbol (i.e. predicate). In the case of logic with equality, it also contains all equations of the form t₁=t₂, where t₁ and t₂ contain no variables.