A ground term or (or gound formula, ground instance, etc.) is a term that does not contain any logical variable.

This should not be confused with a term that does not contain state variables.

Ground terms may and often do contain declared variables and other state variables such as function symbols applied to other ground terms.

See the page on logical variables for an example differentiating logical variables from various state variables and other ground terms.