TOPICS
Search

Ground Literal


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 a literal obtained from those of S by replacing all variables by elements of the Herbrand universe H of S is called a ground literal.


See also

Ground Atom, 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 Literal." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/GroundLiteral.html

Subject classifications