Reference: Chapter 13 of Allen 
Aim: 
To outline a representation of the facts conveyed by NL text, based on firstorder predicate calculus, and to describe how quantifiers can be avoided in this notation by replacing existentially quantified variables by Skolem constants and Skolem functions, and then assuming all remaining variables are universally quantified. 
Keywords: KB, knowledge base, knowledge representation, knowledge representation language, KRL, Skolem functions, skolemization 
Plan: 

∃ x : Person(x) Happy(x) ..... There is a happy person
∀ x : Person(x) Happy(x) ..... All people are happy
eats(john1, X) : fried(X).
means John eats anything
if it's fried.
fried(cartyres1)
is stored in the KB, then eats(john1, cartyres1)
follows.
loves
(x, y)
would be encoded as a formula such as loves(X, sk1)
, where
sk1
is a new constant that stands for the object that is
asserted to exist.
sk1
is called a Skolem constant.
loves
(x,y)
would be encoded as a formula such as loves(sk2(Y), Y)
,
where sk2
is a new function that produces a potentially new
object for each value of Y
.
loves
(x,y) means "for everybody (y), there
is somebody (x) that loves them." So sk2(Y)
is the
somebody that loves Y
.
Summary: Knowledge Representation 
A taste of knowledge representation has been presented, with emphasis on the use of Skolem functions and constants 
CRICOS Provider Code No. 00098G
Copyright (C) Bill Wilson, 2003, except where another source is acknowledged.