Skolemization in Artificial Intelligence

Skolemization:-

Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization (sometimes spelled Skolemnization). The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable

Reduction to Skolem normal form is a method for removing existential quantifiers from formal logic statements.it is the super standard normal form. Skolemization eliminates existential quantifiers by replacing each existentially quantified variable with a Skolem constant or Skolem function.

There are somerules that are followed when we convert first order predict logic into into skolem standard form:-

1. Convert FOPL into PNF(Prenex Normal Form),if it is not in PNF
2. Convert PNF into CNF(Conjunctive normal form)
3. Apply skolemization

Read complete article click here

Originally published at https://pywix.blogspot.com.