Consider a clause (disjunction of literals) obtained from those of a first-order
logic sentential formula 
in Skolemized form
 |
then a clause obtained from those of 
by replacing all variables by elements of the Herbrand
universe 
of 
is called a ground clause.
