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 V_{U} | Constant with symbol space rif:iri | tr(i) = "i"^^rif:iri |

Blank node x in B | Variable symbols ?x | tr(x) = ?x |

Plain literal without a language tag xxx in V_{PL} | Constant with the datatype xsd:string | tr("xxx") = "xxx"^^xsd:string |

Plain literal with a language tag (xxx,lang) in V_{PL} | Constant with the datatype rif:text | tr("xxx"@lang) = "xxx@lang"^^rif:text |

Well-typed literal (s,u) in V_{TL} | Constant with the symbol space u | tr("s"^^u) = "s"^^u |

Ill-typed literal (s,u) in V_{TL} | Constant s^^u' with symbol space rif:local which is not used in C | tr("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, tr_{R} and tr_{Q} 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 (tr_{R}) in which variables are Skolemized, i.e. replaced with constant symbols, and one (tr_{Q}) 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 S | Rule set tr_{R}(S) | tr_{R}(S) = the set of all sk(Forall tr(s p o .)) such that s p o . is a triple in S |

Graph S | Condition (query) tr_{Q}(S) | tr_{Q}(S) = Exists tr(x1tr(), ..., xntr() And(t1tr() ... 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 tr_{R}(S1) union ... union tr_{R}(Sn)) entails tr_{Q}(S). C simple-entails an RIF condition φ iff (R union tr_{R}(S1) union ... union tr_{R}(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*,

the unary predicate wellxml

_{V}/1 is interpreted as the set of XML values,the unary predicate illxml

_{V}/1 is interpreted as the set of objects corresponding to ill-typed XML literals in*V*, and_{TL}the unary predicate illD

_{V}/1 is interpreted as the set of objects corresponding to ill-typed literals in*V*, and_{TL}- the unary predicate lit/1 is interpreted as the union of the value spaces of all data types.

## 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

R^{RDF} | = | (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 (*R ^{RDF}* union R union tr

_{R}(S1) union ... union tr

_{R}(Sn)) has a model.

**Theorem** A combination C=<R,{S1,...,Sn}> rdf-entails a generalized RDF graph T iff (*R ^{RDF}* union R union tr

_{R}(S1) union ... union tr

_{R}(Sn)) entails tr

_{Q}(T). C simple-entails an RIF condition φ iff (

*R*union R union tr

^{RDF}_{R}(S1) union ... union tr

_{R}(Sn)) entails φ.

## Embedding RDFS Entailment

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

R^{RDFS} | = | R union^{RDF}( 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 <R_{1},{S1,...,Sn}> is rdfs-satisfiable iff (*R ^{RDFS}* union R

_{1}union tr

_{R}(S1) union ... union tr

_{R}(Sn)) has a model.

**Theorem** A combination <R,{S1,...,Sn}> rdfs-entails generalized RDF graph T iff (*R ^{RDFS}* union R union tr

_{R}(S1) union ... union tr

_{R}(Sn)) entails tr

_{Q}(T). C rdfs -entails an RIF condition φ iff (

*R*union R union tr

^{RDFS}_{R}(S1) union ... union tr

_{R}(Sn)) entails φ.

## Embedding D-Entailment

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

R^{D} | = | R union^{RDFS}( 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 V) union_{TL}( 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 (*R ^{D}* union R union tr

_{R}(S1) union ... union tr

_{R}(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

*V*and

_{TL}`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 (*R ^{D}*) 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 (*R ^{D}* union R union tr

_{R}(S1) union ... union tr

_{R}(Sn)) entails tr

_{Q}(T). C D-entails an RIF condition φ iff (

*R*union R union tr

^{D}_{R}(S1) union ... union tr

_{R}(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.