In the context of logic, a ground atom is an atomic formula where all of its argument terms are ground terms. Let’s break it down:
- An atomic formula (also known as an atom) is a formula with no deeper propositional structure, meaning it contains no logical connectives or equivalently, it has no strict sub-formulas.
- A ground term is a term that does not contain any variables.
So, if P is an n-ary predicate symbol and t1, t2, …, tn are ground terms, then P(t1, t2, …, tn) is a ground atom.
For example, consider a clause (disjunction of literals) obtained from a first-order logic formula. Then an atomic statement obtained by replacing all variables by values is called a ground atom.
