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 VU | 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 VPL | Constant with the datatype xsd:string | tr("xxx") = "xxx"^^xsd:string |
Plain literal with a language tag (xxx,lang) in VPL | Constant with the datatype rif:text | tr("xxx"@lang) = "xxx@lang"^^rif:text |
Well-typed literal (s,u) in VTL | Constant with the symbol space u | tr("s"^^u) = "s"^^u |
Ill-typed literal (s,u) in VTL | 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, 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 S | Rule 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 S | Condition (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,
the unary predicate wellxmlV/1 is interpreted as the set of XML values,
the unary predicate illxmlV/1 is interpreted as the set of objects corresponding to ill-typed XML literals in VTL, and
the unary predicate illDV/1 is interpreted as the set of objects corresponding to ill-typed literals in VTL, and
- 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
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.