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