Skolemization - Artificial Intelligence Tutorial

Skolemization - Artificial Intelligence

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 some  rules 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

Related Other Post

• Expert System in Artificial Intelligence
• Semantic Network in Artificial Intelligence
• Horn Clause in Artifiial Intelligence
• A* Search Algorithm
• Best First Search Algorithm

• Remove all existential variable with new skolemization constant (A Skolem constant is a function of no variables.)) if there is no universal quantifier before related existential quantifier. Remove existential quantifier.
• Remove all existential variable with new skolemization function if there are universal quantifier before related to existential quantifier.in another word an existential variable is replaced by a Skolem function of all the universal variables to its left. Remove existential quantifier.

Example:-

Ask question #Pywix

• Facebook Page :- https://www.facebook.com/rgrahulgarg786
• Twitter :- https://twitter.com/rgrahulgarg786
• Instagram:- https://www.instagram.com/rahulgupta.786/
• youTube:- https://www.youtube.com/pywixclasses

Please Like, Comment, Share and Subscribe THANK YOU!