unicode_fol_kit.skolemize

unicode_fol_kit.skolemize(node)

Return prenex NNF with existentials replaced by Skolem terms.

Each ∃-bound variable becomes a Skolem function of the universals in scope (a Skolem constant if there are none); the existential quantifiers are dropped and the universal prefix is retained. Satisfiability-preserving.

Parameters:

node (Node)

Return type:

Node