RDF in RIF

I had an action (285) to propose a text for combining RDF with RIF core,
based on an axiomatization of the RDF semantics, embedding blank nodes
as Skolem constants.

A question is which semantics of RDF (simple entailment, RDF entailment,
RDFS entailment, and extensional RDFS entailment) we want to be able to
use in RIF.  We will probably need a mechanism in the syntax to say
which kind of entailment is required.  In the remainder I will speak
about RDFS entailment, but this can easily be parameterized.

I propose the following text about interoperation between RDF and RIF:

Interoperation between RIF and RDF is achieved by embedding RDF graphs
as sets of RIF facts, and by axiomatizing the semantics of RDFS
entailment using a set of RIF rules.

== Embedding of symbols ==

RDF defines four kinds of symbols:
- URIs
- blank nodes
- plain literals
- typed literals

By the RDFS semantics, every symbol is interpreted as a resource.  RIF
defines the sort rif:iri, which corresponds to the set of RDFS
resources.  Hence, the embedding of every RDF symbol will be a member of
the sort rif:iri.

[JB: we might as well use rdfs:Resource directly as a sort; this might
be a sub-sort of rif:iri, or rif:iri might be a sub-sort of rdfs:Resource]

We use a function tr_S which maps RDF symbols occurring in an RDF graph
S to RIF symbols.

tr_S maps RDF URIs  to symbols of the sort rif:iri: tr_S(URI) =
"URI"^^rif:iri

tr_S maps each blank node name x in the graph S to a new globally unique
constant symbol gensym(x,S) of the sort IRI: tr_S(x) =
"gensym(x,S)"^^rif:iri


For the embedding of plain literals in RIF we use the sort rdfs:Literal,
which is a sub-sort of rif:iri:

[JB: another possible way to embed both plain and typed literals is by
using typing]

tr_S maps plain literals "xxx" to symbols of the sort rdfs:Literal:
tr_S("xxx") = "xxx"^^rdfs:Literal

[JB: we need to discuss how to embed the language tag; this could be
done, for example, by declaring sub-sorts of rdfs:Literal for the
respective languages]


[JB: For typed literals, I am not yet entirely sure about the embedding;
in my work on embedding RDF in F-Logic, I have not yet treated literals.
 Several issues come into play such as the special treatment of
rdf:XMLLiteral, and the semantics of other types which may or may not be
taken into account.  Therefore, the following is a rough first sketch of
the embedding.]

For the embedding of typed literals "xxx"^^type-uri in RDF, the URI of
the type is used as the URI of the sort in RIF. rdf:XMLLiteral will have
to be declared a sub-sort of rdfs:Literal.

tr_S maps typed literals "xxx"^^rdf:XMLLiteral where xxx is a valid XML
literal to symbols of the sort XMLLiteral: tr_S("xxx"^^XMLLiteral) =
"xxx"^^XMLLiteral

tr_S maps typed literals "xxx"^^rdf:XMLLiteral where xxx is not a valid
XML literal to symbols of the sort rif:iri: tr_S("xxx"^^XMLLiteral) =
"\"xxx\"^^XMLLiteral"^^rif:iri [assuming the symbol \ is used for
escaping characters]

tr_S maps typed literals "xxx"^^type-uri to symbols of the sort
type-uri: tr_S("xxx"^^type-uri) = "xxx"^^type-uri

[JB: Note that type-uri will have to be declared as a sub-sort of rif:iri]


== Embeddings of triples and graphs ==

[JB: I use the frame syntax below; however, predicate syntax or slotted
 syntax could be used as well, since there is no disjointness between
sorts in RIF]

An RDF graph S is a set of triples of the form (s,p,o), where s, p, and
o are RDF symbols. We extend the mapping function tr_S to embed triples
as RIF facts.

tr_S maps triples (s, p, o) to RIF facts: tr_S((s, p, o)) = Forall
tr_S(s)[tr_S(p) -> tr_S(o)]

tr_S naturally extends to RDF graphs S: tr_S(S) = { tr_S((s, p, o) | (s,
p, o)\in S}

== Embedding of the RDFS semantics ==

A set of additional facts and rules is required to axiomatize the RDFS
semantics.

First, we need to declare the relationships between the various sorts we
use.  Depending on how sub-sort are declared, So_S is a set of rules
axiomatizing the sorts:

So_S = Forall ?X (X^^rif:iri :- X^^rdfs:Literal)
       Forall ?X (X^^rdfs:Literal :- X^^rdf:XMLLiteral)
       {Forall ?X (X^^rif:iri :- X^^type-uri) | type-uri is used as the
type of a typed literal in S}

We then need to axiomatize the axiomatic triples as a set A of RIF facts:

A = {tr_S(a) | a is an RDFS axiomatic triple}

[JB:  alternatively, if we want to avoid axiomatizing an infinite number
of axiomatic triples, we could axiomatize only the relevant triples
(i.e. those involving vocabulary occurring in S and its context, i.e.
the RIF rules)]

Finally, we need to axiomatize the RDFS semantic conditions through a
number of RIF rules R:

R_S = Forall ?X(?X[rdf:type->rdfs:Resource] :- ?X^^rif:iri)
      Forall ?X(?X[rdf:type->rdfs:Literal] :- ?X^^rdfs:Literal)
      {Forall ?X(?X[rdf:type->type-uri] :- ?X^^type-uri) | type-uri is
used as the type of a typed literal in S}
      Forall ?X,?Y,?Z(?X[rdf:type->rdf:Property] :-  ?Y[?X->?Z])
      Forall ?X(?X[rdfs:subPropertyOf->?X :- ?X[rdf:type->rdf:Property)
      ...  [JB:  the rest is all fairly standard]

[JB:  some more thought might be required to work out the desired
relationship between sorts and types (e.g. rdfs:Resource vs sort rif:iri
and type rdfs:Literal vs sort rdfs:Literal)]


Now, the embedding of an RDF  graph S with RDFS semantics is:
tr_S(S) \cup So_S \cup A \cup R




Best, Jos

-- 
Please note my new email address:
                         debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
In heaven all the interesting people are
missing.
  - Friedrich Nietzsche