In mathematical logic, a ground term of a formal system is a term that does not contain any variables.
Similarly, a ground formula is a formula that does not contain any variables.
In first-order logic with identity with constant symbols
Consider the following expressions in first order logic over a signature containing the constant symbols
for the numbers 0 and 1, respectively, a unary function symbol
What follows is a formal definition for first-order languages.
the set of constant symbols,
the set of functional operators, and
the set of predicate symbols.
Ground terms may be defined by logical recursion (formula-recursion): Roughly speaking, the Herbrand universe is the set of all ground terms.
A ground predicate, ground atom or ground literal is an atomic formula all of whose argument terms are ground terms.
Roughly speaking, the Herbrand base is the set of all ground atoms,[1] while a Herbrand interpretation assigns a truth value to each ground atom in the base.
A ground formula or ground clause is a formula without variables.
Ground formulas may be defined by syntactic recursion as follows: Ground formulas are a particular kind of closed formulas.