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.
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).
It's not clear that naming the KIF Object class is essential; the KIF spec specifies it incompletely, so we could identify KIF:Object with RDF:Resource without running into any conflicts that I can see.
hmm... KIF spec doesn't say (=> (real ?x)
(complex ?x)) nor that every integer and rational is
real. I suppose that's to allow for construction of the complex
numbers as, e.g. pairs of reals. But the result doesn't imply that
integers are numbers. Odd.
similarly
everything else.
hm... identify KIF natural number constants with rdf:_1, rdf:_2,
etc? i.e. ContainerMembershipPropertys?
weakly true; cf section 10.3 Changing Levels of Denotation
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:
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.)
@@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...
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...
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)) ) )
plus: inference engines (prolog, algernon, etc.) instrumented to write out proofs. See also: Euler proof mechanism by Jos De Roo of AGFA.
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:
<listof>
<holds/> <!-- @@hmm... if a statement is a triple,
this shouldn't be here. -->
<constant n="...#prop"/>
<constant n="mid:x@y"/>
<string v="val"/>
</listof>
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"/>
becomes
(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.
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