The process of removing all the existential quantifiers from a formula is known as Skolemization. The result is a formula in Skolem normal form that is equivalent in computational complexity to the original. This Demonstration shows the rewriting process of a Skolemization step by step for all general cases up to three quantifier alternations and seven variables or constants.


  • [Snapshot]
  • [Snapshot]
  • [Snapshot]
    • Share:

Embed Interactive Demonstration New!

Just copy and paste this snippet of JavaScript code into your website or blog to put the live Demonstration on your site. More details »

Files require Wolfram CDF Player or Mathematica.