RIF/OWL 2 RL to RIF/1

From Public Domain Knowledge Bank
Jump to: navigation, search

From: https://www.w3.org/TR/2013/NOTE-rif-owl-rl-20130205/#appendix-translation

8 Appendix: OWL 2 RL to RIF translation

The static set of rules in the first appendix provides a complete translation of the OWL 2 RL rules into RIF. While that rule set is within the RIF Core dialect it is fairly inefficient, for example in its handling of lists rules.

In practice we would expect many OWL 2 RL implementations to instantiate the ruleset for a particular ontology. The instantiation process only depends upon OWL TBox axioms and the instantiated ruleset can be applied to other ontologies which only differ by virtue of the ABox assertions.

We here define an algorithm for instantiating a RIF Core rule set for a given OWL 2 RL ontology.

Input: An ontology O conforming to the OWL 2 RL profile and the corresponding translation of O into an RDF Graph RDF(O) as specified in the OWL 2 Mapping to RDF Graphs [OWL 2 RDF Mapping].

Output: A RIF Core rule set R(RDF(O)) such that the RIF-RDF combination of R(RDF(O)) and RDF(O) has the same entailments as the combination R and RDF(O) where R is the static OWL 2 RL rule set defined above.

Algorithm: R(RDF(O)) = FixedRules ∪ templateRules( RDF(O) )

Where the set of FixedRules and the two algorithms templateRules are defined below.

Editor's Note: These rules are believed to be correct. However, since the original version was developed various manual edits have been made to conform to changes in RIF and OWL 2 RL. Mechanical verification will be required before final publication.

8.1 FixedRules

The FixedRule ruleset comprises the following rules:

(* <#eq-ref> *)
Forall ?p ?o ?s (
  ?s[owl:sameAs->?s] :- ?s[?p->?o])

(* <#eq-ref1> *)
Forall ?p ?o ?s (
  ?p[owl:sameAs->?p] :- ?s[?p->?o])

(* <#eq-ref2> *)
Forall ?p ?o ?s (
  ?o[owl:sameAs->?o] :- ?s[?p->?o])

(* <#eq-sym> *)
Forall ?x ?y (
  ?y[owl:sameAs->?x] :- ?x[owl:sameAs->?y])

(* <#eq-trans> *)
Forall ?x ?z ?y (
  ?x[owl:sameAs->?z] :- And(
      ?x[owl:sameAs->?y]
      ?y[owl:sameAs->?z]  ))

(* <#eq-rep-s> *)
Forall ?p ?o ?s ?s2 (
  ?s2[?p->?o] :- And(
      ?s[owl:sameAs->?s2]
      ?s[?p->?o]  ))

(* <#eq-rep-p> *)
Forall ?p ?o ?s ?p2 (
  ?s[?p2->?o] :- And(
      ?p[owl:sameAs->?p2]
      ?s[?p->?o]  ))

(* <#eq-rep-o> *)
Forall ?p ?o ?s ?o2 (
  ?s[?p->?o2] :- And(
      ?o[owl:sameAs->?o2]
      ?s[?p->?o]  ))

(* <#eq-diff1> *)
Forall ?x ?y (
  rif:error() :- And(
      ?x[owl:sameAs->?y]
      ?x[owl:differentFrom->?y]  ))

(* <#prp-ap-label> *)
  rdfs:label[rdf:type->owl:AnnotationProperty]

(* <#prp-ap-comment> *)
  rdfs:comment[rdf:type->owl:AnnotationProperty]

(* <#prp-ap-seeAlso> *)
  rdfs:seeAlso[rdf:type->owl:AnnotationProperty]

(* <#prp-ap-isDefinedBy> *)
  rdfs:isDefinedBy[rdf:type->owl:AnnotationProperty]

(* <#prp-ap-deprecated> *)
  owl:deprecated[rdf:type->owl:AnnotationProperty]

(* <#prp-ap-priorVersion> *)
  owl:priorVersion[rdf:type->owl:AnnotationProperty]

(* <#prp-ap-backwardCompatibleWith> *)
  owl:backwardCompatibleWith[rdf:type->owl:AnnotationProperty]

(* <#prp-ap-incompatibleWith> *)
  owl:incompatibleWith[rdf:type->owl:AnnotationProperty]

(* <#prp-dom> *)
Forall ?p ?c ?x ?y (
  ?x[rdf:type->?c] :- And(
      ?p[rdfs:domain->?c]
      ?x[?p->?y]  ))

(* <#prp-rng> *)
Forall ?p ?c ?x ?y (
  ?y[rdf:type->?c] :- And(
      ?p[rdfs:range->?c]
      ?x[?p->?y]  ))

(* <#cls-thing> *)
  owl:Thing[rdf:type->owl:Class]

(* <#cls-nothing1> *)
  owl:Nothing[rdf:type->owl:Class]

(* <#cls-nothing2> *)
Forall ?x (
  rif:error() :- ?x[rdf:type->owl:Nothing])

(* <#cax-sco> *)
Forall ?x ?c1 ?c2 (
  ?x[rdf:type->?c2] :- And(
      ?c1[rdfs:subClassOf->?c2]
      ?x[rdf:type->?c1]  ))

(* <#cax-eqc1> *)
Forall ?x ?c1 ?c2 (
  ?x[rdf:type->?c2] :- And(
      ?c1[owl:equivalentClass->?c2]
      ?x[rdf:type->?c1]  ))

(* <#cax-eqc2> *)
Forall ?x ?c1 ?c2 (
  ?x[rdf:type->?c1] :- And(
      ?c1[owl:equivalentClass->?c2]
      ?x[rdf:type->?c2]  ))

(* <#cax-dw> *)
Forall ?x ?c1 ?c2 (
  rif:error() :- And(
      ?c1[owl:disjointWith->?c2]
      ?x[rdf:type->?c1]
      ?x[rdf:type->?c2]  ))

(* <#scm-cls> *)
Forall ?c (
  ?c[rdfs:subClassOf->?c] :- ?c[rdf:type->owl:Class])

(* <#scm-cls1> *)
Forall ?c (
  ?c[owl:equivalentClass->?c] :- ?c[rdf:type->owl:Class])

(* <#scm-cls2> *)
Forall ?c (
  ?c[rdfs:subClassOf->owl:Thing] :- ?c[rdf:type->owl:Class])

(* <#scm-cls3> *)
Forall ?c (
  owl:Nothing[rdfs:subClassOf->?c] :- ?c[rdf:type->owl:Class])

(* <#scm-sco> *)
Forall ?c1 ?c2 ?c3 (
  ?c1[rdfs:subClassOf->?c3] :- And(
      ?c1[rdfs:subClassOf->?c2]
      ?c2[rdfs:subClassOf->?c3]  ))

(* <#scm-eqc1> *)
Forall ?c1 ?c2 (
  ?c1[rdfs:subClassOf->?c2] :- ?c1[owl:equivalentClass->?c2])

(* <#scm-eqc11> *)
Forall ?c1 ?c2 (
  ?c2[rdfs:subClassOf->?c1] :- ?c1[owl:equivalentClass->?c2])

(* <#scm-eqc2> *)
Forall ?c1 ?c2 (
  ?c1[owl:equivalentClass->?c2] :- And(
      ?c1[rdfs:subClassOf->?c2]
      ?c2[rdfs:subClassOf->?c1]  ))

(* <#scm-op> *)
Forall ?p (
  ?p[rdfs:subPropertyOf->?p] :- ?p[rdf:type->owl:ObjectProperty])

(* <#scm-op1> *)
Forall ?p (
  ?p[owl:equivalentProperty->?p] :- ?p[rdf:type->owl:ObjectProperty])

(* <#scm-dp> *)
Forall ?p (
  ?p[rdfs:subPropertyOf->?p] :- ?p[rdf:type->owl:DatatypeProperty])

(* <#scm-dp1> *)
Forall ?p (
  ?p[owl:equivalentProperty->?p] :- ?p[rdf:type->owl:DatatypeProperty])

(* <#scm-spo> *)
Forall ?p3 ?p2 ?p1 (
  ?p1[rdfs:subPropertyOf->?p3] :- And(
      ?p1[rdfs:subPropertyOf->?p2]
      ?p2[rdfs:subPropertyOf->?p3]  ))

(* <#scm-eqp1> *)
Forall ?p2 ?p1 (
  ?p1[rdfs:subPropertyOf->?p2] :- ?p1[owl:equivalentProperty->?p2])

(* <#scm-eqp11> *)
Forall ?p2 ?p1 (
  ?p2[rdfs:subPropertyOf->?p1] :- ?p1[owl:equivalentProperty->?p2])

(* <#scm-eqp2> *)
Forall ?p2 ?p1 (
  ?p1[owl:equivalentProperty->?p2] :- And(
      ?p1[rdfs:subPropertyOf->?p2]
      ?p2[rdfs:subPropertyOf->?p1]  ))

(* <#scm-dom1> *)
Forall ?p ?c1 ?c2 (
  ?p[rdfs:domain->?c2] :- And(
      ?p[rdfs:domain->?c1]
      ?c1[rdfs:subClassOf->?c2]  ))

(* <#scm-dom2> *)
Forall ?c ?p2 ?p1 (
  ?p1[rdfs:domain->?c] :- And(
      ?p2[rdfs:domain->?c]
      ?p1[rdfs:subPropertyOf->?p2]  ))

(* <#scm-rng1> *)
Forall ?p ?c1 ?c2 (
  ?p[rdfs:range->?c2] :- And(
      ?p[rdfs:range->?c1]
      ?c1[rdfs:subClassOf->?c2]  ))

(* <#scm-rng2> *)
Forall ?c ?p2 ?p1 (
  ?p1[rdfs:range->?c] :- And(
      ?p2[rdfs:range->?c]
      ?p1[rdfs:subPropertyOf->?p2]  ))

(* <#dt-type2> *)
Group (

   Forall ?s ?p ?lt ( ?lt[rdf:type->rdf:PlainLiteral rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-PlainLiteral( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->rdf:XMLLiteral rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-XMLLiteral( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:decimal rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-decimal( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:integer rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-integer( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:nonNegativeInteger rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-nonNegativeInteger( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:nonPositiveInteger rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-nonPositiveInteger( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:positiveInteger rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-positiveInteger( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:negativeInteger rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-negativeInteger( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:long rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-long( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:int rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-int( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:short rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-short( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:byte rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-byte( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:unsignedLong rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-unsignedLong( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:unsignedInt rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-unsignedInt( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:unsignedShort rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-unsignedShort( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:unsignedByte rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-unsignedByte( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:float rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-float( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:double rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-double( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:string rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-string( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:normalizedString rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-normalizedString( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:token rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-token( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:language rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-language( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:Name rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-Name( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:NCName rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-NCName( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:NMTOKEN rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-NMTOKEN( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:boolean rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-boolean( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:hexBinary rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-hexBinary( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:base64Binary rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-base64Binary( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:anyURI rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-anyURI( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:dateTime rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-dateTime( ?lt )) ))

   Forall ?s ?p ?lt ( ?lt[rdf:type->xsd:dateTimeStamp  rdf:type->rdfs:Literal]
                    :- And( ?s[?p->?lt] External( pred:is-literal-dateTimeStamp ( ?lt )) ))

)

(* <#dt-not-type> *)
Group (

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->rdf:PlainLiteral] External(pred:is-literal-not-PlainLiteral( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->rdf:XMLLiteral] External(pred:is-literal-not-XMLLiteral( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:decimal] External(pred:is-literal-not-decimal( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:integer] External(pred:is-literal-not-integer( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:nonNegativeInteger] External(pred:is-literal-not-nonNegativeInteger( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:nonPositiveInteger] External(pred:is-literal-not-nonPositiveInteger( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:positiveInteger] External(pred:is-literal-not-positiveInteger( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:negativeInteger] External(pred:is-literal-not-negativeInteger( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:long] External(pred:is-literal-not-long( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:int] External(pred:is-literal-not-int( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:short] External(pred:is-literal-not-short( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:byte] External(pred:is-literal-not-byte( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:unsignedLong] External(pred:is-literal-not-unsignedLong( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:unsignedInt] External(pred:is-literal-not-unsignedInt( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:unsignedShort] External(pred:is-literal-not-unsignedShort( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:unsignedByte] External(pred:is-literal-not-unsignedByte( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:float] External(pred:is-literal-not-float( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:double] External(pred:is-literal-not-double( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:string] External(pred:is-literal-not-string( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:normalizedString] External(pred:is-literal-not-normalizedString( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:token] External(pred:is-literal-not-token( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:language] External(pred:is-literal-not-language( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:Name] External(pred:is-literal-not-Name( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:NCName] External(pred:is-literal-not-NCName( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:NMTOKEN] External(pred:is-literal-not-NMTOKEN( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:boolean] External(pred:is-literal-not-boolean( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:hexBinary] External(pred:is-literal-not-hexBinary( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:base64Binary] External(pred:is-literal-not-base64Binary( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:anyURI] External(pred:is-literal-not-anyURI( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:dateTime] External(pred:is-literal-not-dateTime( ?lt )) ))

 Forall ?lt (
  rif:error() :- And (
    ?lt[rdf:type->xsd:dateTimeStamp ] External(pred:is-literal-not-dateTimeStamp ( ?lt )) ))

)

(* <#eq-diff1-literal1> *)
Forall ?x ?y ?s1 ?s2 ?p1 ?p2 (
  rif:error() :- And(
      ?s1[?p1->?x]  ?s2[?p2->?y]
      ?x[owl:sameAs->?y]
      External(pred:literal-not-identical(?x ?y))  ))

(* <#eq-diff1-literal2> *)
Forall ?x ?y ?s1 ?s2 ?p1 ?p2 (
  rif:error() :- And(
      ?s1[?p1->?x]  ?s2[?p2->?y]
      ?x = ?y
      ?x[owl:differentFrom->?y]  ))
                 
(* <#dt-type1-PlainLiteral> *) rdf:PlainLiteral[rdf:type -> rdfs:Datatype]
(* <#dt-type1-decimal> *) xsd:decimal[rdf:type -> rdfs:Datatype]
(* <#dt-type1-integer> *) xsd:integer[rdf:type -> rdfs:Datatype]
(* <#dt-type1-double> *) xsd:double[rdf:type -> rdfs:Datatype]
(* <#dt-type1-string> *) xsd:string[rdf:type -> rdfs:Datatype]
(* <#dt-type1-dateTime> *) xsd:dateTime[rdf:type -> rdfs:Datatype]
(* <#dt-type1-XMLLiteral> *) rdf:XMLLiteral[rdf:type -> rdfs:Datatype]
(* <#dt-type1-Literal> *) rdfs:Literal[rdf:type -> rdfs:Datatype]
(* <#dt-type1-nonNegativeInteger> *) xsd:nonNegativeInteger[rdf:type -> rdfs:Datatype]
(* <#dt-type1-nonPositiveInteger> *) xsd:nonPositiveInteger[rdf:type -> rdfs:Datatype]
(* <#dt-type1-positiveInteger> *) xsd:positiveInteger[rdf:type -> rdfs:Datatype]
(* <#dt-type1-negativeInteger> *) xsd:negativeInteger[rdf:type -> rdfs:Datatype]
(* <#dt-type1-long> *) xsd:long[rdf:type -> rdfs:Datatype]
(* <#dt-type1-int> *) xsd:int[rdf:type -> rdfs:Datatype]
(* <#dt-type1-short> *) xsd:short[rdf:type -> rdfs:Datatype]
(* <#dt-type1-byte> *) xsd:byte[rdf:type -> rdfs:Datatype]
(* <#dt-type1-unsignedLong> *) xsd:unsignedLong[rdf:type -> rdfs:Datatype]
(* <#dt-type1-unsignedInt> *) xsd:unsignedInt[rdf:type -> rdfs:Datatype]
(* <#dt-type1-unsignedShort> *) xsd:unsignedShort[rdf:type -> rdfs:Datatype]
(* <#dt-type1-unsignedByte> *) xsd:unsignedByte[rdf:type -> rdfs:Datatype]
(* <#dt-type1-normalizedString> *) xsd:normalizedString[rdf:type -> rdfs:Datatype]
(* <#dt-type1-token> *) xsd:token[rdf:type -> rdfs:Datatype]
(* <#dt-type1-language> *) xsd:language[rdf:type -> rdfs:Datatype]
(* <#dt-type1-Name> *) xsd:Name[rdf:type -> rdfs:Datatype]
(* <#dt-type1-NCName> *) xsd:NCName[rdf:type -> rdfs:Datatype]
(* <#dt-type1-NMTOKEN> *) xsd:NMTOKEN[rdf:type -> rdfs:Datatype]
(* <#dt-type1-float> *) xsd:float[rdf:type -> rdfs:Datatype]
(* <#dt-type1-boolean> *) xsd:boolean[rdf:type -> rdfs:Datatype]
(* <#dt-type1-hexBinary> *) xsd:hexBinary[rdf:type -> rdfs:Datatype]
(* <#dt-type1-base64Binary> *) xsd:base64Binary[rdf:type -> rdfs:Datatype]
(* <#dt-type1-anyURI> *) xsd:anyURI[rdf:type -> rdfs:Datatype]
(* <#dt-type1-dateTimeStamp> *) xsd:dateTimeStamp [rdf:type -> rdfs:Datatype]

8.2 templateRules algorithm

We specify the algorithm for instantiating the template rules by means of a translation table.

The first column gives a set of RDF triple patterns (s p o) where any of the elements can be a variable (indicated with a '?') prefix.

The second column gives a template to be instantiated. For each match of the triple patterns in RDF(O) we generate a binding map which maps each variable in the triple pattern to a corresponding RDF Node in RDF(O). The template should be processed with this binding map, replacing the corresponding variables by their mapped values.

Example 1

For example the pair:
+ Pattern Template
(?p rdf:type owl:SymmetricProperty)
    Forall ?x ?y (
       ?y[?p->?x] :- And(
         ?x[?p->?y] )) 
Applied to an ontology containing the following RDF triples:

 eg:p rdf:type owl:SymmetricProperty .
 eg:q rdf:type owl:SymmetricProperty .



Would emit the follow RIF rules:

Forall ?x ?y (
  ?y[eg:p->?x] :- And(
      ?x[eg:p->?y]  ))

Forall ?x ?y (
  ?y[eg:q->?x] :- And(
      ?x[eg:q->?y]  ))

Additional Notation for templates

In order to specify the list related rules we need to define some addition notation for templates.
Notation Interpretation
{$ rule text $} Emit the rule text substituting any occurrence of variables from the binding map. The outer {$ $} can be omitted in cases where there is no ambiguity.
for(?elt in ?list) {
    template
} 		 ?list is a variable in the pattern which is bound to an RDF List. The for operator iterates over each element of the ?list in turn replacing the binding map for the ?elt variable with the next list entry and processes the enclosed template in the context of that new binding map.
for(?elt in ?list, != ?other) {
    template
} 		 ?list is a variable in the pattern which is bound to an RDF List. The for operator iterates over each element of the ?list in turn, skipping any element identical to ?other, replacing the binding map for the ?elt variable with the next list entry and processes the enclosed template in the context of that new binding map.
$length(?list)$ Used within a template this will be replaced by the length the RDFList bound to ?list.
$i$ Used within a for(?elt in ?list){ template } this will be replaced by the index of the current ?elt.
$i+1$ Used within a for(?elt in ?list){ template } this will be replaced by the index of the current ?elt, plus 1.

Definition of templateRule Algorithm

The templateRule algorithm is defined using this notation by the following set of pattern/template pairs.
Pattern Template
(?p rdf:type owl:FunctionalProperty ) (* <#prp-fp> *)
Forall ?y2 ?x ?y1 (
     ?y1[owl:sameAs->?y2] :- And(
       ?x[?p->?y1]
       ?x[?p->?y2] ))
(?p rdf:type owl:InverseFunctionalProperty ] ) (* <#prp-ifp> *)
Forall ?x1 ?x2 ?y (
     ?x1[owl:sameAs->?x2] :- And(
       ?x1[?p->?y]
       ?x2[?p->?y] ))
(?p rdf:type owl:IrreflexiveProperty) (* <#prp-irp> *)
Forall ?x (
    rif:error() :- And(
       ?x[?p->?x] ))
(?p rdf:type owl:SymmetricProperty) (* <#prp-symp> *)
Forall ?x ?y (
     ?y[?p->?x] :- And(
       ?x[?p->?y] ))
(?p rdf:type owl:AsymmetricProperty) (* <#prp-asyp> *)
Forall ?x ?y (
    rif:error() :- And(
       ?x[?p->?y]
       ?y[?p->?x] ))
(?p rdf:type owl:TransitiveProperty) (* <#prp-trp> *)
Forall ?x ?z ?y (
     ?x[?p->?z] :- And(
       ?x[?p->?y]
       ?y[?p->?z] ))
(?p1 rdfs:subPropertyOf ?p2) (* <#prp-spo1> *)
Forall ?x ?y (
     ?x[?p2->?y] :- And(
       ?x[?p1->?y] ))


(?p1 owl:equivalentProperty ?p2) (* <#prp-eqp1> *)
Forall ?x ?y (
     ?x[?p2->?y] :- And(
       ?x[?p1->?y] ))
(* <#prp-eqp2> *)
Forall ?x ?y (
     ?x[?p1->?y] :- And(
       ?x[?p2->?y] ))
(?p1 owl:propertyDisjointWith ?p2) (* <#prp-pdw> *)
Forall ?x ?y (
    rif:error() :- And(
       ?x[?p1->?y]
       ?x[?p2->?y] ))
(?p1 owl:inverseOf ?p2) (* <#prp-inv1> *)
Forall ?x ?y (
     ?y[?p2->?x] :- And(
       ?x[?p1->?y] ))

(* <#prp-inv2> *)
Forall ?x ?y (
     ?y[?p1->?x] :- And(
       ?x[?p2->?y] ))
(?x owl:someValuesFrom ?y)
(?x owl:onProperty ?p) 		(* <#cls-svf1> *)
Forall ?v ?u (
     ?u[rdf:type->?x] :- And(
       ?u[?p->?v]
       ?v[rdf:type->?y] ))
(?x owl:someValuesFrom owl:Thing)
(?x owl:onProperty ?p) 		(* <#cls-svf2> *)
Forall ?v ?u (
     ?u[rdf:type->?x] :- And(
     ?u[?p->?v] ))
(?x owl:allValuesFrom ?y)
(?x owl:onProperty ?p) 		(* <#cls-avf> *)
Forall ?v ?u (
     ?v[rdf:type->?y] :- And(
       ?u[rdf:type->?x]
       ?u[?p->?v] ))
(?x owl:hasValue ?y)
(?x owl:onProperty ?p) 		(* <#cls-hv1> *)
Forall ?u (
     ?u[?p->?y] :- And(
       ?u[rdf:type->?x] ))

(* <#cls-hv2> *)
    Forall ?u (
       ?u[rdf:type->?x] :- And(
         ?u[?p->?y] ))
(?x owl:maxCardinality 0)
(?x owl:onProperty ?p) 		(* <#cls-maxc1> *)
Forall ?u ?y (
    rif:error() :- And(
       ?u[?p->?y]
       ?u[rdf:type->?x] ))
(?x owl:maxCardinality 1)
(?x owl:onProperty ?p) 		(* <#cls-maxc2> *)
Forall ?y2 ?u ?y1 (
     ?y1[owl:sameAs->?y2] :- And(
       ?u[?p->?y1]
       ?u[?p->?y2]
       ?u[rdf:type->?x] ))
(?x owl:maxQualifiedCardinality 0)
(?x owl:onProperty ?p)
(?x owl:onClass ?c) 		(* <#cls-maxqc1> *)
Forall ?u ?y (
    rif:error() :- And(
       ?u[rdf:type->?x]
       ?u[?p->?y]
       ?y[rdf:type->?c] ))
(?x owl:maxQualifiedCardinality 0)
(?x owl:onProperty ?p)
(?x owl:onClass owl:Thing) 		(* <#cls-maxqc2> *)
Forall ?y ?u (
    rif:error() :- And(
       ?u[rdf:type->?x]
       ?u[?p->?y] ))


(?x owl:maxQualifiedCardinality 1)
(?x owl:onProperty ?p)
(?x owl:onClass ?c)

(* <#cls-maxqc3> *)

Forall ?y2 ?u ?y1 (
     ?y1[owl:sameAs->?y2] :- And(  ?u[rdf:type->?x]  ?u[?p->?y1]  ?y1[rdf:type->?c]  ?u[?p->?y2]  ?y2[rdf:type->?c] ))
(?x owl:maxQualifiedCardinality 1)
(?x owl:onProperty ?p)
(?x owl:onClass owl:Thing)

(* <#cls-maxqc4> *)

Forall ?y2 ?u ?y1 (
     ?y1[owl:sameAs->?y2] :- And(  ?u[rdf:type->?x]  ?u[?p->?y1]  ?u[?p->?y2] ))
(?c1 owl:hasValue ?i)
(?c1 owl:onProperty ?p1)
(?c2 owl:hasValue ?i)
(?c2 owl:onProperty ?p2) 		(* <#scm-hv> *) 
  ?c1[rdfs:subClassOf->?c2] :- And(
      ?p1[rdfs:subPropertyOf->?p2]  )


(?c1 owl:someValuesFrom ?y1)
(?c1 owl:onProperty ?p)
(?c2 owl:someValuesFrom ?y2)
(?c2 owl:onProperty ?p) 		(* <#scm-svf1> *) 
  ?c1[rdfs:subClassOf->?c2] :- And(
      ?y1[rdfs:subClassOf->?y2]  )


(?c1 owl:someValuesFrom ?y)
(?c1 owl:onProperty ?p1)
(?c2 owl:someValuesFrom ?y)
(?c2 owl:onProperty ?p2) 		(* <#scm-svf2> *) 
  ?c1[rdfs:subClassOf->?c2] :- And(
      ?p1[rdfs:subPropertyOf->?p2]  )
(?c1 owl:allValuesFrom ?y1)
(?c1 owl:onProperty ?p)
(?c2 owl:allValuesFrom ?y2)
(?c2 owl:onProperty ?p) 		(* <#scm-avf1> *) 
  ?c1[rdfs:subClassOf->?c2] :- And(
      ?y1[rdfs:subClassOf->?y2]  )
(?c1 owl:allValuesFrom ?y)
(?c1 owl:onProperty ?p1)
(?c2 owl:allValuesFrom ?y)
(?c2 owl:onProperty ?p2) 		(* <#scm-avf2> *) 
  ?c2[rdfs:subClassOf->?c1] :- And(
      ?p1[rdfs:subPropertyOf->?p2]  )
(?a rdf:type owl:AllDifferent)
(?a owl:members ?l) 		(* <#eq-diff2> *)

for(?x in ?l) { 

for(?y in ?l, != x) {
  {$
  rif:error() :- And (
      ?x[owl:sameAs->?y] )
  $}
}

}

(?a rdf:type owl:AllDifferent)
(?a owl:distinctMembers ?l) 		(* <#eq-diff3> *) for(?x in ?l) {
    for(?y in ?l, != ?X) { {$ rif:error() :- And (  ?x[owl:sameAs->?y] ) $} } }
(?l rdf:type owl:AllDisjointProperties) (* <#prp-adp> *) for(?x in ?l) {
    for(?y in ?l, != ?x) {
      {$ Forall ?o ?v (
        rif:error() :- And (  ?o[?x->?v ?y->?v]) ) $} } }
(?l rdf:type owl:AllDisjointClasses) (* <#cax-adc> *) for(?x in ?l) {
    for(?y in ?l, != ?x) {
      {$ Forall ?something (
        rif:error() :- And (  ?something[rdf:type->?x rdf:type->?y]) ) $} } }
(?p owl:propertyChainAxiom ?pc) (* <#prp-spo2> *)

{$

Forall
    $} for(?next in ?pc) { {$ ?u$i$ $} } {$  ?u$length(?pc)$ (  ?u$0$[?p->?u$length(?pc)$] :- And ( $} for(?next in ?pc) { {$  ?u$i$[?next->?u$i+1$] $} } {$ )) $} (?c owl:hasKey ?u) (* <#prp-key> *) {$ Forall ?x ?y ?v (  ?x[owl:sameAs->?y] :- And (  ?x[rdf:type->?c]  ?y[rdf:type->?c] $} for(?key in ?u) { {$  ?x[?key->?v] ?y[?key->?v] $} } {$ )) $}
(?c owl:intersectionOf ?l) (* <#cls-int2> *)
{$
    Forall ?y (
       ?y[rdf:type->?c] :- And (
    $}
      for(?ty in ?l) {
        {$
           ?y[rdf:type->?ty]
        $}
      }
      {$ )) $}
(?c owl:unionOf ?l) (* <#cls-uni> *)
for(?ci in ?l) {
    {$
      Forall ?y (
         ?y[rdf:type->?c] :- And (
           ?y[rdf:type->?ci] ))
        $}
      }
(?c owl:oneOf ?l) (* <#cls-oo> *)
for(?yi in ?l) {
    {$
       ?yi[rdf:type->?c]
    $}
}
(?c owl:intersectionOf ?l) (* <#scm-int> *)
for(?ci in ?l) {
    {$
      Forall ?y (
         ?y[rdf:type->?ci] :- And (
           ?y[rdf:type->?c] ))
           ?c[rdfs:subClassOf->?ci]
        $}
      }
(?c owl:unionOf ?l) (* <#scm-uni> *)
for(?ci in ?l) {
    {$
       ?ci[rdfs:subClassOf->?c]
    $}
}
(?x owl:sourceIndividual ?i1)
(?x owl:assertionProperty ?p)
(?x owl:targetIndividual ?i2) 		(* <#prp-npa1> *)
    rif:error() :- And(
       ?i1[?p->?i2] )
(?x owl:sourceIndividual ?i1)
(?x owl:assertionProperty ?p)
(?x owl:targetValue ?i2) 		(* <#prp-npa2> *)
    rif:error() :- And(
       ?i1[?p->?i2] )
(?c1 owl:disjointWith ?c2) (* <#cax-dw> *)
Forall ?x (
    rif:error() :- And(
       ?x[rdf:type->?c1]
       ?x[rdf:type->?c2] ))
(?c1 owl:complementOf ?c2 ) (* <#cls-com> *)
Forall ?x (
    rif:error() :- And(
       ?x[rdf:type->?c1]
       ?x[rdf:type->?c2] ))
Retrieved from "https://pdkb.chivanet.org/wiki/index.php?title=RIF/OWL_2_RL_to_RIF/1&oldid=1080"