This is an archive of an inactive wiki and cannot be modified.

RIF-RDF combinations can be embedded into RIF Rule sets in a fairly straightforward way, thereby demonstrating how an RIF-compliant translator without native support for RDF can process RIF-RDF combinations.

For the embedding we use the concrete syntax of RIF and the N-Triples syntax for RDF.

Throughout this section the function tr is defined, which maps symbols, triples, and RDF graphs to RIF symbols, statements, and rule sets.

Embedding Symbols

Given a combination C=< R,S>, the function tr maps RDF symbols of a vocabulary V and a set of blank nodes B to RIF symbols, as defined in following table.

RDF Symbol RIF Symbol Mapping
IRI i in VUConstant with symbol space rif:iritr(i) = "i"^^rif:iri
Blank node x in BVariable symbols ?xtr(x) = ?x
Plain literal without a language tag xxx in VPLConstant with the datatype xsd:stringtr("xxx") = "xxx"^^xsd:string
Plain literal with a language tag (xxx,lang) in VPLConstant with the datatype rif:texttr("xxx"@lang) = "xxx@lang"^^rif:text
Well-typed literal (s,u) in VTLConstant with the symbol space utr("s"^^u) = "s"^^u
Ill-typed literal (s,u) in VTLConstant s^^u' with symbol space rif:local which is not used in Ctr("s"^^u) = "s^^u'"^^rif:local

The embedding is not defined for combinations which include RDF graphs with RDF URI references which are not absolute IRIs.

Embedding Triples and Graphs

The mapping function tr is extended to embed triples as RIF statements. Finally, two embedding functions, trR and trQ embed RDF graphs as RIF rule sets and conditions, respectively. The following section shows how these embeddings can be used for reasoning with combinations.

We define two mappings for RDF graphs, one (trR) in which variables are Skolemized, i.e. replaced with constant symbols, and one (trQ) in which variables are existentially quantified.

The function sk takes as arguments a formula R with variables, and returns a formula R', which is obtained from R by replacing every variable symbol ?x in R with "new-iri"^^rif:iri, where new-iri is a new globally unique IRI.

RDF Construct RIF Construct Mapping
Triple s p o .Property frame tr(s)[tr(p) -> tr(o)]tr(s p o .) = tr(s)[tr(p) -> tr(o)]
Graph SRule set trR(S)trR(S) = the set of all sk(Forall tr(s p o .)) such that s p o . is a triple in S
Graph SCondition (query) trQ(S)trQ(S) = Exists tr(x1), ..., tr(xn) And(tr(t1) ... tr(tm)), where x1, ..., xn are the blank nodes occurring in S and t1, ..., tm are the triples in S

Embedding Simple Entailment

The following theorem shows how checking simple-entailment of combinations can be reduced to checking entailment of RIF conditions by using the embeddings of RDF graphs of the previous section.

Theorem A combination C=<R,{S1,...,Sn}> simple-entails a generalized RDF graph S iff (R union trR(S1) union ... union trR(Sn)) entails trQ(S). C simple-entails an RIF condition φ iff (R union trR(S1) union ... union trR(Sn)) entails φ.

Built-ins required

The embeddings of RDF and RDFS entailment require a number of built-in predicate symbols to be available to appropriately deal with literals.

EDITORS NOTE: It is not yet clear which built-in predicates will be available in RIF. Therefore, the built-ins mentioned in this section may change. Furthermore, built-ins may be axiomatized if they are not provided by the language.

Given a vocabulary V,

Embedding RDF Entailment

We axiomatize the semantics of the RDF vocabulary using the following RIF rules and conditions.

The compact URIs used in the RIF rules in this section and the next are short for the complete URIs with the rif:iri datatype, e.g. rdf:type is short for "http://www.w3.org/1999/02/22-rdf-syntax-ns#type"^^rif:iri

RRDF=(Forall tr(s p o .)) for every RDF axiomatic triple s p o .) union
(Forall ?x ?x[rdf:type -> rdf:Property] :- Exists ?y,?z (?y[?x -> ?z]),
Forall ?x ?x[rdf:type -> rdf:XMLLiteral] :- wellxml(?x),
Forall ?x "1"^^xsd:integer="2"^^xsd:integer :- And(?x[rdf:type -> rdf:XMLLiteral] illxml(?x)))

Theorem A combination <R,{S1,...,Sn}> is rdf-satisfiable iff (RRDF union R union trR(S1) union ... union trR(Sn)) has a model.

Theorem A combination C=<R,{S1,...,Sn}> rdf-entails a generalized RDF graph T iff (RRDF union R union trR(S1) union ... union trR(Sn)) entails trQ(T). C simple-entails an RIF condition φ iff (RRDF union R union trR(S1) union ... union trR(Sn)) entails φ.

Embedding RDFS Entailment

We axiomatize the semantics of the RDF(S) vocabulary using the following RIF rules and conditions.

RRDFS=RRDF union
(Forall tr(s p o .)) for every RDFS axiomatic triple s p o .) union
(Forall ?x ?x[rdf:type -> rdfs:Resource],
Forall ?u,?v,?x,?y ?u[rdf:type -> ?y] :- And(?x[rdfs:domain -> ?y] ?u[?x -> ?v]),
Forall ?u,?v,?x,?y ?v[rdf:type -> ?y] :- And(?x[rdfs:range -> ?y] ?u[?x -> ?v]),
Forall ?x ?x[rdfs:subPropertyOf -> ?x] :- ?x[rdf:type -> rdf:Property],
Forall ?x,?y,?z ?x[rdfs:subPropertyOf -> ?z] :- And (?x[rdfs:subPropertyOf -> ?y] ?y[rdfs:subPropertyOf -> ?z]),
Forall ?x,?y,?z1,?z2 ?z1[y -> ?z2] :- And (?x[rdfs:subPropertyOf -> ?y] ?z1[x -> ?z2]),
Forall ?x ?x[rdfs:subClassOf -> rdfs:Resource] :- ?x[rdf:type -> rdfs:Class],
Forall ?x,?y,?z ?z[rdf:type -> ?y] :- And (?x[rdfs:subClassOf -> ?y] ?z[rdf:type -> ?x]),
Forall ?x ?x[rdfs:subClassOf -> ?x] :- ?x[rdf:type -> rdfs:Class],
Forall ?x,?y,?z ?x[rdfs:subClassOf -> ?z] :- And (?x[rdfs:subClassOf -> ?y] ?y[rdfs:subClassOf -> ?z]),
Forall ?x ?x[rdfs:subPropertyOf -> rdfs:member] :- ?x[rdf:type -> rdfs:ContainerMembershipProperty],
Forall ?x ?x[rdfs:subClassOf -> rdfs:Literal] :- ?x[rdf:type -> rdfs:Datatype],
Forall ?x ?x[rdf:type -> rdfs:Literal] :- lit(?x),
Forall ?x "1"^^xsd:integer="2"^^xsd:integer :- And(?x[rdf:type -> rdfs:Literal] illxml(?x)))

Theorem A combination <R1,{S1,...,Sn}> is rdfs-satisfiable iff (RRDFS union R1 union trR(S1) union ... union trR(Sn)) has a model.

Theorem A combination <R,{S1,...,Sn}> rdfs-entails generalized RDF graph T iff (RRDFS union R union trR(S1) union ... union trR(Sn)) entails trQ(T). C rdfs -entails an RIF condition φ iff (RRDFS union R union trR(S1) union ... union trR(Sn)) entails φ.

Embedding D-Entailment

We axiomatize the semantics of the data types using the following RIF rules and conditions.

RD=RRDFS union
(Forall u[rdf:type -> rdfs:Datatype] | for every IRI in the domain of D) union
(Forall "s"^^u[rdf:type -> "u"^^rif:iri] | for every well-typed literal (s , u ) in VTL) union
(Forall ?x, ?y dt(?x,?y) :- And(?x[rdf:type -> ?y] ?y[rdf:type -> rdfs:Datatype]),
Forall ?x "1"^^xsd:integer="2"^^xsd:integer :- And(?x[rdf:type -> rdfs:Literal] illD(?x))`))

Theorem A combination <R,{S1,...,Sn}>, where R does not contain the equality symbol, is D-satisfiable iff (RD union R union trR(S1) union ... union trR(Sn)) is satisfiable and does not entail Exists ?x And(dt(?x,u) dt(?x,u')) for any two URIs u and u' in the domain of D such that the value spaces of D(u) and D(u') are disjoint, and does not entail Exists ?x dt(s^^u,"u'"^^rif:iri) for any (s, u) in VTL and u' in the domain of D such that s is not in the lexical space of D(u').

EDITOR'S NOTE: Since this condition is very complex we might consider to discard this theorem, and suggest the above set of rules (RD) as an approximation of the semantics.

Theorem A D-satisfiable combination <R,{S1,...,Sn}>, where R does not contain the equality symbol, D-entails a generalized RDF graphs T iff (RD union R union trR(S1) union ... union trR(Sn)) entails trQ(T). C D-entails an RIF condition φ iff (RD union R union trR(S1) union ... union trR(Sn)) entails φ.

EDITOR'S NOTE: The restriction to equality-free rule sets is necessary because D-interpretations impose stronger conditions on the interpretation of typed literals in case different datatype URIs are equal than RIF does.