Replacing an existentially quantified variable by a fresh Skolem function of the preceding universally quantified variables. A witness independent of all universal variables is represented by a fresh constant. The operation preserves satisfiability after expanding the first-order signature; it is not generally logical equivalence for arbitrary interpretations of the new symbols.
A first-order sentence consisting of a block of universal quantifiers followed by a quantifier-free formula, obtained by Skolemization in an expanded first-order signature. Its matrix can additionally be put into conjunctive normal form to obtain clausal form.

Ancestors (10)

  1. Skolem function
  2. Skolem hull
  3. Elementary substructure
  4. First-order structure
  5. First-order logic
  6. Mathematical logic
  7. Foundations of mathematics
  8. Area of mathematics
  9. Mathematics
  10. Home

Incoming links (8)

View article source

Discussion (0) New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version