Transcript WG2-NYC2-006-KIF Presentation

Knowledge Interchange Format
Michael Gruninger
National Institute of Standards and
Technology
[email protected]
What is KIF?
• Knowledge
Interchange Format
(KIF) is a language
designed for use in
the interchange of
knowledge among
disparate computer
systems
What is Knowledge?
• Facts
– William is the brother of Harold.
– Charles is not the brother of George.
• Statements/Rules/Constraints
– The mother of Charles is either Elizabeth or Ann.
– Two people are siblings if and only if they are brother
or sister.
– Every person has a mother.
How Will KIF be Used?
• Specification of ontologies
– Standard Upper Ontology
– Process Specification Language
– Semantic Web
• Software agent communication
• Automated deduction and constraint
satisfaction
Features of KIF
 The language has a declarative semantics.
 The language is logically comprehensive.
 The
language
provides
for
the
representation
of
knowledge
about
knowledge.
Organization of KIF
• Part 1 (KIF-Core) : syntax and semantics of a
language equivalent to first-order logic.
• Part 2 (Sorted KIF) specifies the syntax and
semantics for class hierarchies.
• Part 3 (MetaKIF) syntax and semantics of the
metatheory of KIF-Core.
Scope of KIF Core
Language of first-order logic:
Language with logical symbols for
– connectives (conjunction, disjunction, negation,
implication, equivalence),
– equality,
– quantifiers (existential and universal)
Example KIF Sentences
The mother of Charles is either Elizabeth or Ann.
(forall (?x)
(=>
(mother Charles ?x)
(or
(= ?x Elizabeth)
(= ?x Ann))))
Everyone’s age must be greater than 0.
(forall (?x)
(greater (age ?x) 0))
Example KIF Sentences
Nobody can be both a brother and a sister.
(forall (?x ?y)
(=> (bother ?x ?y)
(not (sister ?x ?y))))
Every person has a mother.
(forall (?x)
(=>
(person ?x)
(exists (?y)
(and
(person ?y)
(mother ?x ?y)))))
Example KIF Sentences
Two people are siblings if and only if they are
brother or sister.
(forall (?x ?y)
(=> (and
(<=>
(person ?x)
(person ?y))
(sibling ?x ?y)
(or
(brother ?x ?y)
(sister ?x ?y)))))
Semantics: Intuitions
• A universe of discourse is the set of all
objects within some domain.
• Terms are used to denote objects in the
universe.
• For every set of objects, a function
associates a unique object in the universe.
• For every set of objects, a relation
associates a truth value.
Semantics: Structures
• A structure consists of a nonempty set O
together with the functions:
– Interpretation function 
– Semantic valuation function 
– Satisfaction function 
Semantics: Models
• A structure satisfies a sentence  if and
only if () = true
• A structure is a model of a theory T if and
only if it satisfies each sentence in T
• A theory T entails a sentence  if and only
if every model of T satisfies .
Inference
• A proof system consists of a set of KIF
sentences and a set of inference rules that
transform sentences into new ones.
• A sentence  is provable from a theory T if
and only if  can be generated by applying
a finite number of inference rules to the
sentences of T.
Compliance
• A proof system is compliant with KIF if and
only if:
– It is sound -- every sentence that is provable
from a theory is entailed by the theory.
– It is complete -- every sentence that is entailed
by a theory is provable from the theory.
Additional Features
• KIF-Core also allows quantification over
relations and functions that are denoted by
words in the lexicon of a theory.
(forall (?r ?x ?y)
(<=>
(symmetric ?r)
(<=> (?r ?x ?y)
(?r ?y ?x))))
Next Steps
• Incorporation of namespaces for KIF
modules
• Semantics for sequence variables
• Syntax and semantics for Sorted-KIF
• Syntax and semantics for MetaKIF