Consider a clause (disjunction of literals) obtained from those of a first-order
logic formula 
in Skolemized form
 |
Then an atomic statement obtained from those of 
by replacing all variables by elements
of the Herbrand universe 
of 
is called a ground atom. The set of all ground atoms that can be formed from predicate
symbols from 
and terms from 
is called the Herbrand base.
