TOPICS
Search

Ground Clause


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

  forall x_1... forall x_nS,

then a clause obtained from those of S by replacing all variables by elements of the Herbrand universe H of S is called a ground clause.


See also

Ground Atom, Ground Literal, Herbrand Base, Herbrand Universe

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

Explore with Wolfram|Alpha

Cite this as:

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

Subject classifications