W3C SW Dev

Knowledge Interchange Format (KIF) as an RDF Schema

This page provides a home for the terms from [KIF] in the web.

We hereby define each URIs beginning with http://www.w3.org/2000/07/hs78/KIF?word= to denote the KIF word following the =, after %xx un-escaping (cf 4.3 Lexems in [KIF]). Watch out for things that aren't XML names! Remember to %xx escape non URI characters[@@cite]. Use lowercase hex digits.

We start with the KIF universe of discourse, from section 5 Basics.

Different users of a declarative representation language, like KIF, are likely to have different universes of discourse. KIF is conceptually promiscuous in that it does not require every user to share the same universe of discourse. On the other hand, KIF is conceptually grounded in that every universe of discourse is required to include certain basic objects.

Classes of KIF Objects

We identify KIF one-place relations with RDF Classes. Note that these are sets of lists of length one, not sets of class members directly. (we could say that formally in KIFv3, but dpansKIF doesn't have sets.)

We formalize the claim that an RDF statement is a triple by making it a subclass of kif triple.

The distinction between URIs and URI references parallels the distinction between words and strings in KIF: URIs map 1-1 to URI references. Note that the reverse mapping for URI references takes an extra parameter, the base URI.

Note that spelling here follows the KIF spec, where it defines the corresponding word. We follow the RDF convention that class names begin with capital letters for classes that the KIF spec does not define a word for (@@these need to go in a different namespace; they break rdf2kif.xsl).

List Utilities

This obsoletes my earlier list schema.

This document is intended to contain all the relations from [KIF], but I'm adding to it in a sort of "on-demand" basis. I need these right away:

Characters and Strings

KIF characters are ASCII characters, and hence Unicode characters; these map neatly into RDF. Going the other way is not as straightforward. It's not a problem for symbols, since there is already an encoding of Unicode characters in URIs[@@cite], but there may be no KIF string corresponding to an RDF string.

We can make up the difference by requiring the inclusion of a new set of objects in the universe of discourse: the set of Unicode characters (we get strings for free by the inclusion of "All finite lists of objects in the universe of discourse.")

A KIF word corresponds roughly to a URI (i.e. an absoluteURI with optional fragment identifer) in RDF.


If a kif constant r conforms to URI syntax (e.g. http\://example.org), we map it to a URIwf directly; otherwise, we map r to concat("http://www.w3.org/2000/07/hs78/KIF?constant=", r). (@@refined above for indvar, seqvar, operators, and maybe numerals.)

Unwinding functional terms

@@what did Ora say the conventional term is?

RDF has no syntax for functional terms, but we can regard each function as a relation, so that (f x) denotes some y such that f'(x, y) where f' is the relation constant corresponding to f. (@@which convention to use for the n-ary case?)

@@... and so on...

Proof checking infrastructure

Syntactic sugar/notation:

(defrelation rdf.subject (?statement ?resource) :=
  (holds \h\t\t\p\://\w\w\w.\w\3.\o\r\g/1999/02/22-\r\d\f-\s\y\n\t\a\x-\n\s\#\s\u\b\j\e\ct ?statement ?resource)
(defrelation rdf.predicate (?statement ?resource) :=
  (holds http\://www.w3.org/1999/02/22-rdf-syntax-ns\#predicate ?statement ?resource)
(defrelation rdf.object (?statement ?resource) :=
  (holds http\://www.w3.org/1999/02/22-rdf-syntax-ns\#subject ?statement ?resource)
(defobject rdf.Statement := \h\t\t\p...@@)

ok... but that's pretty boring; i.e. it gives you ground 2-place predicates, quantification, and metaknowledge (reification). But it doesn't give you logical connectives (and/or/not) nor equality. Hence the next level, swell...

Reification Axioms

I think these are the axioms that relate reification in RDF to quoting in KIF:

(defrelation reify (?st ?pred ?subj ?obj) :=
   (and (rdf.Statement ?st) (rdf.predicate ?st ?pred) (rdf.subject ?st ?subj) (rdf.object ?st ?obj)))
(defobj swell.equal ...@@...)
(defobj swell.nand ...@@..)
(defobj swell.exists ...@@...) ; RDF doesn't give it a name

; unquoting equality literals
(forall ((?st rdf.Statement)  ?x ?y)
  (=> (reify ?st swell.equal ?x ?y)
      (= ?st ^(= ,?x ,?y))) )

; unquoting logicals (using the scheffer(sp?) stroke trick)
(forall ((?st rdf.Statement)  ?p ?q)
  (=> (reify ?st swell.nand ?p ?q)
      (= ?st ^(not (and ,?p ,?q))) ) )

; unquoting existentials
(forall ((?st rdf.Statement) ?v ?p)
  (=> (reify ?st swell.exists ?v ?p)
      (= ?st ^(exists ,?v ,?p)) ) )

; unquoting lists
; hmm... generalize this to all functional relations,
; ala KIF 3/OKBC?
(forall ((?st rdf.Statement) ?l ?i)
  (=> (reify ?st swell.first ?l ?i)
      (= ?st ^(= (first ,?l) ,?i)) ) )

(forall ((?st rdf.Statement) ?l ?r)
  (=> (reify ?st swell.rest ?l ?r)
      (= ?st ^(= (rest ,?l) ,?r)) ) )

; 1-place predicates
(<=> (holds rdf.type ?I ?C)
     (holds ?C ?I))

; unquoting n-ary predicates
(forall ((?st rdf.Statement) ?pred ?args)
  (=> (refiy ?st swell.holds ?pred ?args)
      (= ?st (append ^(holds ,?pred) ?args)) ) )

; unquoting all other 2-place predicates
(forall ((?st rdf.Statement) ?p ?s ?o)
  (=> (not (item ?p '(swell.equal swell.nand swell.exists
                      swell.first swell.rest swell.holds
                      ) ) )
      (reify ?st ?p ?s ?o)
      (= ?st ^(holds ,?p ,?s ,?o)) ) )

; toplevel logical operator(s)
(forall ((?st rdf.Statement))
  (=> (holds swell.nand ?p ?q)
    (wtr ^(not (and ,?p ,?q)) ) )

; toplevel equality
(forall (?x ?y)
  (=> (holds swell.equal ?x ?y)
      (wtr ^(= ,?x ,?y)) ) )

; toplevel n-ary
(forall (?pred ?args)
  (=> (holds swell.holds ?pred ?args)
      (wtr (append ^(holds ,?pred) ?args)) ) )

; toplevel existential
(forall (?v ?uri ?st)
  (=> (holds swell.exists ?v ?st)
      (not-free-in ?v ?st)
      (list ?st)
    (wtr ^(exists (,?v) ,(subst ?v ?uri ?st)) ) )

Proof checking infrastructure: @@TODO:

plus: inference engines (prolog, algernon, etc.) instrumented to write out proofs. See also: Euler proof mechanism by Jos De Roo of AGFA.

Converting RDF to KIF

In case there are KIF tools we can leverage, I have developed another RDF parser in XSLT (earlier XSLT RDF parser) to spit out KIF[KIF] so that a statement

<rdf:Description about="mid:x@y" foo:prop="val"/>

gets wrtten out as:

  <holds/> <!-- @@hmm... if a statement is a triple,
                this shouldn't be here. -->
  <constant n="...#prop"/>
  <constant n="mid:x@y"/>
  <string v="val"/>

and then I have kifOutput.java, an XT output mode, that writes this out as

(holds ...\p\r\o\p \m\i\d\:\x\@\y "val")

Note that KIF words are case-folded, except for escaped characters. So we have to escape just about everything.

Anonymous nodes

<rdf:Description prop="val"/>

become existentials:

(exists (?gen1) (holds ...prop ?gen1 "val"))

@@this is broken: variables get recognized by the parser:

<Description about="...hs78/KIF#%3fp" prop="val"/>


(holds ...prop ?p "val")

For an XML literal value, use the RDF schema in the infoset spec to reify it. Done: content.xsl, but not integrated.

Diversion: Some KIF History

I found a KIF home page, not to be confused with the KIF home page (i.e. the top one from the google query and the one cited from the semantic web roadmap).

KIF Version 3.0 of Wed Dec 7 13:23:42 PST 1994 : includes sets, and an interesting treatment of paradoxes; different treatment of the level-breaking paradox too. Hmm... interesting bits on semantics; esp , which might be useful for operational/protocol semantics.

hah! speaking of RDF (a DAG model) and KIF (an s-expression syntax), there's a thread on wffs and graphs around 25 Feb 1994.

Some interesting standards-politics in there too, including:

What I was trying to say was that there is an established principle in academics that reviews are performed by anonymous and disinterested parties.

Ginsberg 20 Dec 93

and Parallel standards projects for KIF and CGs from John Sowa, 28 Apr 1994

more fun bits...

The higher-orderist can only reply that when he uses his higher-order quantifiers he *means* (bang the table, stamp the foot) full-blown higher-order quantification; he *intends* to be quantifying over the full power set of his domain.

Chris Menzel 19 Dec 1993


Knowledge Interchange Format draft proposed American National Standard (dpANS) NCITS.T2/98-004
Last Modified: Thursday, 25-Jun-98 22:31:37 GMT

Dan Connolly
$Revision: 1.37 $ of $Date: 2000/08/14 08:05:34 $ by $Author: connolly $