TOPICS
Search

Ground Atom


Consider a clause (disjunction of literals) obtained from those of a first-order logic formula Phi in Skolemized form

  forall x_1... forall x_nS.

Then an atomic statement obtained from those of S by replacing all variables by elements of the Herbrand universe H of S is called a ground atom. The set of all ground atoms that can be formed from predicate symbols from S and terms from H is called the Herbrand base.


See also

Atomic Statement, Ground Clause, Herbrand Base, Herbrand Universe

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

Cite this as:

Sakharov, Alex. "Ground Atom." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/GroundAtom.html

Subject classifications