Skolemization

Requires a Wolfram Notebook System
Interact on desktop, mobile and cloud with the free Wolfram Player or other Wolfram Language products.
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.
Contributed by: Hector Zenil (March 2011)
Open content licensed under CC BY-NC-SA
Snapshots
Details
detailSectionParagraphPermanent Citation
"Skolemization"
http://demonstrations.wolfram.com/Skolemization/
Wolfram Demonstrations Project
Published: March 7 2011