First-Order Logic Knowledge Interchange Format (KIF)

Knowledge Systems Laboratory, Stanford University

Logical Sentences: => <= <=>

uImplication – (=> <sentence>* <sentence>)

E.g., (=> (On A B) (On B C))

8TIV((=> antecedent1 … antecedentn consequent)) =

>true when:

–TIV(antecedenti) is false for some I = 1, … , n; or

–TIV (consequent) is true

>false otherwise

E.g., (=> (On A D) (On D D))

8TIV((=> a1 … an c)) = TIV((or (not a1) … (not an) c))

uImplication – (<= <sentence> <sentence>*)

uLogical equivalence – (<=> <sentence> <sentence>)

8TIV ((sent1 <=> sent2)) =

>true when TIV (sent1) = TIV (sent2)

>false otherwise

8TIV((<=> s1 s2)) = TIV((and (=> s1 s2) (=> s2 s1)))