Skolem function - p3

Tóm lại: skolem functions dùng để khử   và 

Trong số các ví dụ đã post ở phần p1 và p2, thì ví dụ sau đây là dễ hiểu nhất, súc tích nhất và cô đọng nhất.
-->

Steps to convert a sentence to clause form:

Eliminate all <=> connectives by replacing each instance of the form (P <=> Q) by expression ((P => Q) ^ (Q => P))

Eliminate all => connectives by replacing each instance of the form (P => Q) by (~P v Q)

Reduce the scope of each negation symbol to a single predicate by applying equivalences such as converting
~~P to P
~(P v Q) to ~P ^ ~Q
~(P ^ Q) to ~P v ~Q
~(Ax)P to (Ex)~P
~(Ex)P to (Ax)~P

Standardize variables: rename all variables so that each quantifier has its own unique variable name. For
example, convert (Ax)P(x) to (Ay)P(y) if there is another place where variable x is already used.

Eliminate existential quantification by introducing Skolem functions. For example, convert (Ex)P(x) to
P(c) where c is a brand new constant symbol that is not used in any other sentence. c is called a Skolem
constant.
More generally, if the existential quantifier is within the scope of a universal quantified
variable, then introduce a Skolem function that depends on the universally quantified variable.
For example, (Ax)(Ey)P(x,y) is converted to (Ax)P(x, f(x)). f is called a Skolem function, and must be a
brand new function name that does not occur in any other sentence.
Example: (Ax)(Ey)loves(x,y) is converted to (Ax)loves(x,f(x)) where in this case f(x) specifies the
person that x loves.
(If we knew that everyone loved their mother, then f could stand for the mother-of function.)

Remove universal quantification symbols by first moving them all to the left end and making the scope of
each the entire sentence, and then just dropping the "prefix" part. E.g., convert (Ax)P(x) to P(x)

Distribute "and" over "or" to get a conjunction of disjunctions called conjunctive normal form.
convert (P ^ Q) v R to (P v R) ^ (Q v R)
convert (P v Q) v R to (P v Q v R)

Split each conjunct into a separate clause, which is just a disjunction ("or") of negated and nonnegated
predicates, called literals

Standardize variables apart again so that each clause contains variable names that do not occur in any
other clause

Examples:

Convert the sentence
(Ax)(P(x) => ((Ay)(P(y) => P(f(x,y))) ^ ~(Ay)(Q(x,y) => P(y))))

Eliminate <=> Nothing to do here.

Eliminate => (Ax)(~P(x) v ((Ay)(~P(y) v P(f(x,y))) ^ ~(Ay)(~Q(x,y) v P(y))))

Reduce scope of negation (Ax)(~P(x) v ((Ay)(~P(y) v P(f(x,y))) ^ (Ey)(Q(x,y) ^ ~P(y))))

Standardize variables (Ax)(~P(x) v ((Ay)(~P(y) v P(f(x,y))) ^ (Ez)(Q(x,z) ^ ~P(z))))

Eliminate existential quantification (Ax)(~P(x) v ((Ay)(~P(y) v P(f(x,y))) ^ (Q(x,g(x)) ^ ~P(g(x)))))

Drop universal quantification symbols (~P(x) v ((~P(y) v P(f(x,y))) ^ (Q(x,g(x)) ^ ~P(g(x)))))

Convert to conjunction of disjunctions (~P(x) v ~P(y) v P(f(x,y))) ^ (~P(x) v Q(x,g(x))) ^ (~P(x) v
~P(g(x)))

Create separate clauses
~P(x) v ~P(y) v P(f(x,y))
~P(x) v Q(x,g(x))
~P(x) v ~P(g(x))

Standardize variables
~P(x) v ~P(y) v P(f(x,y))
~P(z) v Q(z,g(z))
~P(w) v ~P(g(w))