First-Order Logic Knowledge Interchange Format (KIF)

Knowledge Systems Laboratory, Stanford University

Existentially Quantified Sentences

u(exists <individual variable> <sentence>)

E.g, (exists ?b (On ?b table))

(forall ?b1 (or (on ?b1 table) (exists ?b2 (On ?b1 ?b2))))

8TIV((exists ?var sent)) =

>true when TIV’(sent) = true

for some version V’ of V with respect to variable ?var

>false otherwise

u(exists (<individual variable>*) <sentence>)

E.g., (exists (?b1 ?b2) (and (On ?b1 ?A) (Above ?A ?b2)))

8TIV ((exists (?var1 … ?varn) sent)) =

>true when TIV’(sent) = true

for some version V’ of V with respect to ?var1 … ?varn

>false otherwise

uforall not in the scope of an exists may be omitted

E.g, (or (on ?b1 table) (exists ?b2 (On ?b1 ?b2)))