Difference between revisions of "RIF/OWL 2 RL to RIF/1"

From Public Domain Knowledge Bank
Jump to: navigation, search
(→‎Definition of templateRule Algorithm)
 
(9 intermediate revisions by the same user not shown)
Line 598: Line 598:
 
!--><UL>      ?x[?p->?y1] <br><!--
 
!--><UL>      ?x[?p->?y1] <br><!--
 
!--></UL><UL>      ?x[?p->?y2]  ))
 
!--></UL><UL>      ?x[?p->?y2]  ))
 +
 
|-
 
|-
 
| (?p rdf:type owl:InverseFunctionalProperty ] )
 
| (?p rdf:type owl:InverseFunctionalProperty ] )
Line 608: Line 609:
 
!-->
 
!-->
  
−
|+
+
|-
−
(?p rdf:type owl:IrreflexiveProperty)
+
| (?p rdf:type owl:IrreflexiveProperty)
−
(* <#prp-irp> *)
+
 
−
Forall ?x (
+
| (* <#prp-irp> *) <br><!--
−
  rif:error() :- And(
+
!-->Forall ?x ( <br><!--
−
      ?x[?p->?x]  ))
+
!--><UL>  rif:error() :- And( <br><!--
−
(?p rdf:type owl:SymmetricProperty)
+
!--><UL>      ?x[?p->?x]  ))
−
(* <#prp-symp> *)
+
 
−
Forall ?x ?y (
+
|-
−
  ?y[?p->?x] :- And(
+
| (?p rdf:type owl:SymmetricProperty)
−
      ?x[?p->?y]  ))
+
 
−
(?p rdf:type owl:AsymmetricProperty)
+
| (* <#prp-symp> *) <br><!--
−
(* <#prp-asyp> *)
+
!-->Forall ?x ?y ( <br><!--
−
Forall ?x ?y (
+
!--><UL>  ?y[?p->?x] :- And( <br><!--
−
  rif:error() :- And(
+
!--><UL>      ?x[?p->?y]  ))
−
      ?x[?p->?y]
+
 
−
      ?y[?p->?x]  ))
+
|-
−
(?p rdf:type owl:TransitiveProperty)
+
| (?p rdf:type owl:AsymmetricProperty)
−
(* <#prp-trp> *)
+
 
−
Forall ?x ?z ?y (
+
| (* <#prp-asyp> *) <br><!--
−
  ?x[?p->?z] :- And(
+
!-->Forall ?x ?y ( <br><!--
−
      ?x[?p->?y]
+
!--><UL>  rif:error() :- And( <br><!--
−
      ?y[?p->?z]  ))
+
!--><UL>      ?x[?p->?y] <br><!--
−
(?p1 rdfs:subPropertyOf ?p2)
+
!--></ul><UL>  ?y[?p->?x]  ))
−
(* <#prp-spo1> *)
+
 
−
Forall ?x ?y (
+
|-
−
  ?x[?p2->?y] :- And(
+
| (?p rdf:type owl:TransitiveProperty)
−
      ?x[?p1->?y]  ))
+
 
−
(?p1 owl:equivalentProperty ?p2)
+
| (* <#prp-trp> *) <br><!--
−
(* <#prp-eqp1> *)
+
!-->Forall ?x ?z ?y ( <br><!--
−
Forall ?x ?y (
+
!--><UL>  ?x[?p->?z] :- And(<br><!--
−
  ?x[?p2->?y] :- And(
+
!--><UL>      ?x[?p->?y]<br><!--
−
      ?x[?p1->?y]  ))
+
!--></UL><ul>  ?y[?p->?z]  ))
−
(* <#prp-eqp2> *)
+
 
−
Forall ?x ?y (
+
|-
−
  ?x[?p1->?y] :- And(
+
| (?p1 rdfs:subPropertyOf ?p2)
−
      ?x[?p2->?y]  ))
+
 
−
(?p1 owl:propertyDisjointWith ?p2)
+
| (* <#prp-spo1> *)<br><!--
−
(* <#prp-pdw> *)
+
!-->Forall ?x ?y ( <br><!--
−
Forall ?x ?y (
+
!--><UL>  ?x[?p2->?y] :- And( <br><!--
−
  rif:error() :- And(
+
!--><UL>      ?x[?p1->?y]  ))<br><!--
−
      ?x[?p1->?y]
+
!-->
−
      ?x[?p2->?y]  ))
+
 
−
(?p1 owl:inverseOf ?p2)
+
 
−
(* <#prp-inv1> *)
+
|-
−
Forall ?x ?y (
+
|  (?p1 owl:equivalentProperty ?p2)
−
  ?y[?p2->?x] :- And(
+
 
−
      ?x[?p1->?y]  ))
+
| (* <#prp-eqp1> *)<br><!--
 +
!-->Forall ?x ?y ( <br><!--
 +
!--><UL>  ?x[?p2->?y] :- And( <br><!--
 +
!--><UL>      ?x[?p1->?y]  ))
 +
 
 +
<br></UL></UL><!--
 +
!-->(* <#prp-eqp2> *)<br><!--
 +
!-->Forall ?x ?y ( <br><!--
 +
!--><UL>  ?x[?p1->?y] :- And( <br><!--
 +
!--><UL>      ?x[?p2->?y]  ))
 +
 
 +
|-
 +
| (?p1 owl:propertyDisjointWith ?p2)
 +
 
 +
| (* <#prp-pdw> *) <br><!--
 +
!-->Forall ?x ?y ( <br><!--
 +
!--><UL>  rif:error() :- And( <br><!--
 +
!--><UL>      ?x[?p1->?y] <br><!--
 +
!--></UL><UL>  ?x[?p2->?y]  ))
 +
 
 +
|-
 +
| (?p1 owl:inverseOf ?p2)
 +
 
 +
| (* <#prp-inv1> *)           <br><!--
 +
!-->Forall ?x ?y (             <br><!--
 +
!--><UL>  ?y[?p2->?x] :- And( <br><!--
 +
!--><UL>      ?x[?p1->?y]  )) <br><!--
 +
!--></UL></UL>
 +
 
 +
<br><!--
 +
!-->(* <#prp-inv2> *)          <br><!--
 +
!-->Forall ?x ?y (              <br><!--
 +
!--><UL>  ?y[?p1->?x] :- And(  <br><!--
 +
!--><UL>      ?x[?p2->?y]  ))
 +
 
 +
|-
 +
|    (?x owl:someValuesFrom ?y) <br><!--
 +
!--> (?x owl:onProperty ?p)
 +
 
 +
| (* <#cls-svf1> *)                <br><!--
 +
!-->Forall ?v ?u (                  <br><!--
 +
!--><UL>  ?u[rdf:type->?x] :- And( <br><!--
 +
!--><UL>      ?u[?p->?v]          <br><!--
 +
!--></UL><UL>  ?v[rdf:type->?y]  ))
 +
 
 +
|-
 +
|    (?x owl:someValuesFrom owl:Thing) <br><!--
 +
!--> (?x owl:onProperty ?p)
 +
 
 +
| (* <#cls-svf2> *)                <br><!--
 +
!-->Forall ?v ?u (                  <br><!--
 +
!--><UL>  ?u[rdf:type->?x] :- And( <br><!--
 +
!-->      ?u[?p->?v]  ))
 +
 
 +
|-
 +
|    (?x owl:allValuesFrom ?y) <br><!--
 +
!--> (?x owl:onProperty ?p)
 +
 
 +
| (* <#cls-avf> *)                  <br><!--
 +
!-->Forall ?v ?u (                  <br><!--
 +
!--><UL>  ?v[rdf:type->?y] :- And( <br><!--
 +
!--><UL>      ?u[rdf:type->?x]    <br><!--
 +
!--></UL><UL>  ?u[?p->?v]  ))
 +
 
 +
|-
 +
|    (?x owl:hasValue ?y)          <br><!--
 +
!--> (?x owl:onProperty ?p)
 +
 
 +
| (* <#cls-hv1> *)                  <br><!--
 +
!-->Forall ?u (                    <br><!--
 +
!--><UL>  ?u[?p->?y] :- And(      <br><!--
 +
!--><UL>      ?u[rdf:type->?x]  )) <br><!--
 +
!--></UL></UL>
 +
 
 +
<br><!--
 +
!-->(* <#cls-hv2> *)                <br><!--
 +
!--><UL>Forall ?u (                <br><!--
 +
!--><UL>  ?u[rdf:type->?x] :- And( <br><!--
 +
!--><UL>      ?u[?p->?y]  ))
 +
 
 +
|-
 +
|    (?x owl:maxCardinality 0)      <br><!--
 +
!--> (?x owl:onProperty ?p)
 +
 
 +
| (* <#cls-maxc1> *)                <br><!--
 +
!-->Forall ?u ?y (                  <br><!--
 +
!--><UL>  rif:error() :- And(      <br><!--
 +
!--><UL>      ?u[?p->?y]          <br><!--
 +
!--></UL><UL>  ?u[rdf:type->?x]  ))
 +
 
 +
|-
 +
|    (?x owl:maxCardinality 1)      <br><!--
 +
!--> (?x owl:onProperty ?p)
 +
 
 +
| (* <#cls-maxc2> *)                    <br><!--
 +
!-->Forall ?y2 ?u ?y1 (                <br><!--
 +
!--><UL>  ?y1[owl:sameAs->?y2] :- And( <br><!--
 +
!--><UL>      ?u[?p->?y1]              <br><!--
 +
!--></UL><UL>  ?u[?p->?y2]              <br><!--
 +
!--></UL><UL>  ?u[rdf:type->?x]  ))
 +
 
 +
|-
 +
|    (?x owl:maxQualifiedCardinality 0) <br><!--
 +
!--> (?x owl:onProperty ?p)            <br><!--
 +
!--> (?x owl:onClass ?c)
 +
 
 +
| (* <#cls-maxqc1> *)                    <br><!--
 +
!-->Forall ?u ?y (                      <br><!--
 +
!--><UL>  rif:error() :- And(          <br><!--
 +
!--><UL>      ?u[rdf:type->?x]          <br><!--
 +
!--></UL><UL>  ?u[?p->?y]                <br><!--
 +
!--></UL><UL>  ?y[rdf:type->?c]  ))
 +
 
 +
|-
 +
|    (?x owl:maxQualifiedCardinality 0)  <br><!--
 +
!--> (?x owl:onProperty ?p)              <br><!--
 +
!--> (?x owl:onClass owl:Thing)
 +
 
 +
| (* <#cls-maxqc2> *)                    <br><!--
 +
!-->Forall ?y ?u (                      <br><!--
 +
!--><UL>  rif:error() :- And(          <br><!--
 +
!--><UL>      ?u[rdf:type->?x]          <br><!--
 +
!--></UL><UL>  ?u[?p->?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 (
+
|   (?x owl:maxQualifiedCardinality 1) <br><!--
−
   ?u[rdf:type->?x] :- And(
+
!--> (?x owl:onProperty ?p)             <br><!--
−
      ?u[?p->?y]  ))
+
!--> (?x owl:onClass ?c)
−
(?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> *)
 
(* <#cls-maxqc3> *)
−
Forall ?y2 ?u ?y1 (
+
Forall ?y2 ?u ?y1 ( <br><!--
 +
!--><UL>
 
   ?y1[owl:sameAs->?y2] :- And(
 
   ?y1[owl:sameAs->?y2] :- And(
 
       ?u[rdf:type->?x]
 
       ?u[rdf:type->?x]
Line 735: Line 795:
 
       ?u[?p->?y2]
 
       ?u[?p->?y2]
 
       ?y2[rdf:type->?c]  ))
 
       ?y2[rdf:type->?c]  ))
−
(?x owl:maxQualifiedCardinality 1)  
+
 
−
(?x owl:onProperty ?p)  
+
|-
−
(?x owl:onClass owl:Thing)
+
|    (?x owl:maxQualifiedCardinality 1)   <br><!--
 +
!--> (?x owl:onProperty ?p)               <br><!--
 +
!--> (?x owl:onClass owl:Thing)
 +
 
 
(* <#cls-maxqc4> *)
 
(* <#cls-maxqc4> *)
−
Forall ?y2 ?u ?y1 (
+
Forall ?y2 ?u ?y1 ( <br><!--
 +
!--><UL>
 
   ?y1[owl:sameAs->?y2] :- And(
 
   ?y1[owl:sameAs->?y2] :- And(
 
       ?u[rdf:type->?x]
 
       ?u[rdf:type->?x]
 
       ?u[?p->?y1]
 
       ?u[?p->?y1]
 
       ?u[?p->?y2]  ))
 
       ?u[?p->?y2]  ))
−
(?c1 owl:hasValue ?i)
+
 
−
(?c1 owl:onProperty ?p1)
+
|-
−
(?c2 owl:hasValue ?i)
+
|    (?c1 owl:hasValue ?i)             <br><!--
−
(?c2 owl:onProperty ?p2)
+
!--> (?c1 owl:onProperty ?p1)         <br><!--
−
(* <#scm-hv> *)
+
!--> (?c2 owl:hasValue ?i)             <br><!--
 +
!--> (?c2 owl:onProperty ?p2)
 +
 
 +
| (* <#scm-hv> *)
 
   ?c1[rdfs:subClassOf->?c2] :- And(
 
   ?c1[rdfs:subClassOf->?c2] :- And(
 
       ?p1[rdfs:subPropertyOf->?p2]  )
 
       ?p1[rdfs:subPropertyOf->?p2]  )
−
(?c1 owl:someValuesFrom ?y1)
+
 
−
(?c1 owl:onProperty ?p)
+
 
−
(?c2 owl:someValuesFrom ?y2)
+
|-
−
(?c2 owl:onProperty ?p)
+
|    (?c1 owl:someValuesFrom ?y1)   <br><!--
−
(* <#scm-svf1> *)
+
!--> (?c1 owl:onProperty ?p)         <br><!--
 +
!--> (?c2 owl:someValuesFrom ?y2)   <br><!--
 +
!--> (?c2 owl:onProperty ?p)
 +
 
 +
| (* <#scm-svf1> *)
 
   ?c1[rdfs:subClassOf->?c2] :- And(
 
   ?c1[rdfs:subClassOf->?c2] :- And(
 
       ?y1[rdfs:subClassOf->?y2]  )
 
       ?y1[rdfs:subClassOf->?y2]  )
−
(?c1 owl:someValuesFrom ?y)
+
 
−
(?c1 owl:onProperty ?p1)
+
 
−
(?c2 owl:someValuesFrom ?y)
+
|-
−
(?c2 owl:onProperty ?p2)
+
|    (?c1 owl:someValuesFrom ?y)   <br><!--
−
(* <#scm-svf2> *)
+
!--> (?c1 owl:onProperty ?p1)       <br><!--
 +
!--> (?c2 owl:someValuesFrom ?y)   <br><!--
 +
!--> (?c2 owl:onProperty ?p2)
 +
 
 +
| (* <#scm-svf2> *)
 
   ?c1[rdfs:subClassOf->?c2] :- And(
 
   ?c1[rdfs:subClassOf->?c2] :- And(
 
       ?p1[rdfs:subPropertyOf->?p2]  )
 
       ?p1[rdfs:subPropertyOf->?p2]  )
−
(?c1 owl:allValuesFrom ?y1)
+
 
−
(?c1 owl:onProperty ?p)
+
|-
−
(?c2 owl:allValuesFrom ?y2)
+
|    (?c1 owl:allValuesFrom ?y1)   <br><!--
−
(?c2 owl:onProperty ?p)
+
!--> (?c1 owl:onProperty ?p)       <br><!--
−
(* <#scm-avf1> *)
+
!--> (?c2 owl:allValuesFrom ?y2)   <br><!--
 +
!--> (?c2 owl:onProperty ?p)
 +
 
 +
| (* <#scm-avf1> *)
 
   ?c1[rdfs:subClassOf->?c2] :- And(
 
   ?c1[rdfs:subClassOf->?c2] :- And(
 
       ?y1[rdfs:subClassOf->?y2]  )
 
       ?y1[rdfs:subClassOf->?y2]  )
−
(?c1 owl:allValuesFrom ?y)
+
 
−
(?c1 owl:onProperty ?p1)
+
|-
−
(?c2 owl:allValuesFrom ?y)
+
|    (?c1 owl:allValuesFrom ?y)   <br><!--
−
(?c2 owl:onProperty ?p2)
+
!--> (?c1 owl:onProperty ?p1)     <br><!--
−
(* <#scm-avf2> *)
+
!--> (?c2 owl:allValuesFrom ?y)   <br><!--
 +
!--> (?c2 owl:onProperty ?p2)
 +
 
 +
| (* <#scm-avf2> *)
 
   ?c2[rdfs:subClassOf->?c1] :- And(
 
   ?c2[rdfs:subClassOf->?c1] :- And(
 
       ?p1[rdfs:subPropertyOf->?p2]  )
 
       ?p1[rdfs:subPropertyOf->?p2]  )
−
(?a rdf:type owl:AllDifferent)
+
 
−
(?a owl:members ?l)
+
|-
−
(* <#eq-diff2> *)
+
|    (?a rdf:type owl:AllDifferent)   <br><!--
 +
!--> (?a owl:members ?l)
 +
 
 +
| (* <#eq-diff2> *)
 
for(?x in ?l) {
 
for(?x in ?l) {
 
  for(?y in ?l, != x) {
 
  for(?y in ?l, != x) {
Line 790: Line 874:
 
  }
 
  }
 
}
 
}
−
(?a rdf:type owl:AllDifferent)
+
 
−
(?a owl:distinctMembers ?l)
+
|-
−
(* <#eq-diff3> *)
+
|    (?a rdf:type owl:AllDifferent)   <br><!--
−
for(?x in ?l) {
+
!--> (?a owl:distinctMembers ?l)
 +
 
 +
| (* <#eq-diff3> *)
 +
for(?x in ?l) { <br><!--
 +
!--><UL>
 
  for(?y in ?l, != ?X) {
 
  for(?y in ?l, != ?X) {
 
   {$
 
   {$
Line 801: Line 889:
 
  }
 
  }
 
}
 
}
−
(?l rdf:type owl:AllDisjointProperties)
+
 
−
(* <#prp-adp> *)
+
|-
−
for(?x in ?l) {
+
| (?l rdf:type owl:AllDisjointProperties)
−
for(?y in ?l, != ?x) {
+
 
−
  {$
+
| (* <#prp-adp> *)
−
  Forall ?o ?v (
+
for(?x in ?l) { <br><!--
−
  rif:error() :- And (
+
!--><UL> for(?y in ?l, != ?x) { <br><!--
 +
!--><UL>  {$
 +
  Forall ?o ?v (   <br><!--
 +
!--><UL>  rif:error() :- And (
 
       ?o[?x->?v ?y->?v]) )
 
       ?o[?x->?v ?y->?v]) )
 
   $}
 
   $}
 
  }
 
  }
 
}
 
}
−
(?l rdf:type owl:AllDisjointClasses)
+
 
−
(* <#cax-adc> *)
+
|-
−
for(?x in ?l) {
+
| (?l rdf:type owl:AllDisjointClasses)
−
  for(?y in ?l, != ?x) {
+
 
 +
| (* <#cax-adc> *)
 +
for(?x in ?l) { <br><!--
 +
!--><UL>
 +
  for(?y in ?l, != ?x) { <br><!--
 +
!--><UL>
 
   {$
 
   {$
−
  Forall ?something (
+
  Forall ?something ( <br><!--
 +
!--><UL>
 
   rif:error() :- And (
 
   rif:error() :- And (
 
       ?something[rdf:type->?x rdf:type->?y]) )
 
       ?something[rdf:type->?x rdf:type->?y]) )
Line 823: Line 920:
 
  }
 
  }
 
}
 
}
−
(?p owl:propertyChainAxiom ?pc)
+
 
−
(* <#prp-spo2> *)
+
|-
 +
| (?p owl:propertyChainAxiom ?pc)
 +
 
 +
| (* <#prp-spo2> *)
 
{$
 
{$
−
  Forall  
+
  Forall <br><!--
 +
!--><UL>
 
  $}
 
  $}
 
for(?next in ?pc) {  
 
for(?next in ?pc) {  
Line 836: Line 937:
 
   ?u$0$[?p->?u$length(?pc)$] :- And (
 
   ?u$0$[?p->?u$length(?pc)$] :- And (
 
$}
 
$}
−
for(?next in ?pc) {
+
for(?next in ?pc) {  
 
   {$
 
   {$
 
     ?u$i$[?next->?u$i+1$]
 
     ?u$i$[?next->?u$i+1$]
Line 855: Line 956:
 
}
 
}
 
{$ )) $}       
 
{$ )) $}       
−
(?c owl:intersectionOf ?l)
+
 
−
(* <#cls-int2> *)
+
|-
−
{$
+
| (?c owl:intersectionOf ?l)
−
Forall ?y (
+
 
−
  ?y[rdf:type->?c] :- And (
+
| (* <#cls-int2> *)                 <br><!--
−
$}
+
!--> {$                             <br><!--
−
for(?ty in ?l) {
+
!--><ul> Forall ?y (                 <br><!--
−
  {$
+
!--><ul>  ?y[rdf:type->?c] :- And ( <br><!--
−
    ?y[rdf:type->?ty]
+
!--></ul> $}                         <br><!--
−
$}    
+
!--><ul> for(?ty in ?l) {         <br><!--
−
}  
+
!--><ul> {$                       <br><!--
−
{$ )) $}       
+
!--><ul>    ?y[rdf:type->?ty]     <br><!--
−
(?c owl:unionOf ?l)
+
!--></ul> $}                       <br><!--
−
(* <#cls-uni> *)
+
!--></ul> }                       <br><!--
−
for(?ci in ?l) {
+
!--> {$ )) $}       
−
  {$
+
 
−
   Forall ?y (
+
|-
−
     ?y[rdf:type->?c] :- And (
+
| (?c owl:unionOf ?l)
−
      ?y[rdf:type->?ci] ))
+
 
−
$}
+
| (* <#cls-uni> *)                       <br><!--
−
}  
+
!--> for(?ci in ?l) {                     <br><!--
−
(?c owl:oneOf ?l)
+
!--><ul> {$                             <br><!--
−
(* <#cls-oo> *)
+
!--><ul>   Forall ?y (                   <br><!--
−
for(?yi in ?l) {
+
!--><ul>     ?y[rdf:type->?c] :- And (   <br><!--
−
{$
+
!--><ul>          ?y[rdf:type->?ci] ))   <br><!--
−
  ?yi[rdf:type->?c]
+
!--></ul> $}                             <br><!--
−
  $}
+
!--></ul>}  
−
}
+
 
−
(?c owl:intersectionOf ?l)
+
|-
−
(* <#scm-int> *)
+
| (?c owl:oneOf ?l)
−
for(?ci in ?l) {
+
 
−
{$
+
| (* <#cls-oo> *)             <br><!--
−
  Forall ?y (
+
!--> for(?yi in ?l) {         <br><!--
−
    ?y[rdf:type->?ci] :- And (
+
!--><ul>  {$                 <br><!--
−
       ?y[rdf:type->?c] ))
+
!--><ul>    ?yi[rdf:type->?c] <br><!--
−
     
+
!--></ul> $}                 <br><!--
−
  ?c[rdfs:subClassOf->?ci]
+
!--></ul> }
−
$}
+
 
−
}
+
|-
−
(?c owl:unionOf ?l)
+
| (?c owl:intersectionOf ?l)
−
(* <#scm-uni> *)
+
 
−
for(?ci in ?l) {
+
| (* <#scm-int> *)                       <br><!--
−
  {$
+
!-->for(?ci in ?l) {                     <br><!--
−
  ?ci[rdfs:subClassOf->?c]
+
!--><ul> {$                             <br><!--
−
$}
+
!--><ul>  Forall ?y (                   <br><!--
−
}
+
!--><ul>    ?y[rdf:type->?ci] :- And ( <br><!--
−
(?x owl:sourceIndividual ?i1)
+
!--><ul>       ?y[rdf:type->?c] ))     <br><!--
−
(?x owl:assertionProperty ?p)
+
!--></ul><ul>  ?c[rdfs:subClassOf->?ci] <br><!--
−
(?x owl:targetIndividual ?i2)
+
!--></ul> $}                             <br><!--
−
(* <#prp-npa1> *)
+
!--></ul>}
−
  rif:error() :- And(
+
 
−
      ?i1[?p->?i2]  )
+
|-
−
(?x owl:sourceIndividual ?i1)
+
| (?c owl:unionOf ?l)
−
(?x owl:assertionProperty ?p)
+
 
−
(?x owl:targetValue ?i2)
+
| (* <#scm-uni> *)                         <br><!--
−
(* <#prp-npa2> *)
+
!--> for(?ci in ?l) {                       <br><!--
−
  rif:error() :- And(
+
!--><ul> {$                           <br><!--
−
      ?i1[?p->?i2]  )
+
!--><ul>        ?ci[rdfs:subClassOf->?c]   <br><!--
 +
!--></ul> $}                           <br><!--
 +
!--></ul> }
 +
 
 +
|-
 +
|    (?x owl:sourceIndividual ?i1)     <br><!--
 +
!--> (?x owl:assertionProperty ?p)     <br><!--
 +
!--> (?x owl:targetIndividual ?i2)
 +
 
 +
| (* <#prp-npa1> *)         <br><!--
 +
!--><ul> rif:error() :- And( <br><!--
 +
!--><ul>  ?i1[?p->?i2]  )
 +
 
 +
|-
 +
|    (?x owl:sourceIndividual ?i1)   <br><!--
 +
!--> (?x owl:assertionProperty ?p)   <br><!--
 +
!--> (?x owl:targetValue ?i2)
 +
 
 +
| (* <#prp-npa2> *)         <br><!--
 +
!--><ul>  rif:error() :- And( <br><!--
 +
!--><ul>      ?i1[?p->?i2]  )
  
 
|-
 
|-
 
| (?c1 owl:disjointWith ?c2)
 
| (?c1 owl:disjointWith ?c2)
  
−
| (* <#cax-dw> *) <br><!--
+
| (* <#cax-dw> *)               <br><!--
−
!--> Forall ?x ( <br><!--
+
!--> Forall ?x (                 <br><!--
−
!--><UL>  rif:error() :- And( <br><!--
+
!--><UL>  rif:error() :- And(   <br><!--
 
!--><UL>      ?x[rdf:type->?c1] <br><!--
 
!--><UL>      ?x[rdf:type->?c1] <br><!--
 
!--></UL><ul>  ?x[rdf:type->?c2] ))
 
!--></UL><ul>  ?x[rdf:type->?c2] ))
Line 928: Line 1,049:
 
| (* <#cls-com> *) <br><!--
 
| (* <#cls-com> *) <br><!--
 
!--> Forall ?x ( <br><!--
 
!--> Forall ?x ( <br><!--
−
!-->  rif:error() :- And( <br><!--
+
!--><UL>  rif:error() :- And( <br><!--
−
!-->      ?x[rdf:type->?c1] <br><!--
+
!--><UL>      ?x[rdf:type->?c1] <br><!--
−
!-->       ?x[rdf:type->?c2] ))
+
!--></UL><ul>  ?x[rdf:type->?c2] ))
 
|}
 
|}

Latest revision as of 00:40, 9 November 2019

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"