OWLRL

From RIF

Jump to: navigation, search


Document title:
OWL 2 RL in RIF
Editor
Dave Reynolds, Hewlett Packard Laboratories

Contents

1 Introduction

OWL 2 RL is a syntactic subset (profile) of OWL 2 that is amenable to implementation using rule-based technologies. The OWL 2 Profiles document provides a partial axiomatization of the OWL 2 RDF-Based Semantics in the form of first-order implications that can be used as the basis for such an implementation.

This note describes how that axiomatization can be expressed as a set of RIF rules within the RIF Core dialect.

A complete translation to RIF is not possible due to a mismatch in the supported datatypes between RIF and OWL 2. However, a subset of OWL 2 RL restricted to the RIF datatypes can be implemented via RIF rules.

2 Summary of issues

The rules for the OWL 2 RL semantics can be divided into four (non-disjoint) categories of rules.

Triple pattern rules derive one or more RDF triples from a conjunction of RDF triple patterns. Translation of these to RIF by means of Frame formulae is trivial.

List rules involve processing of RDF lists in the input graph and are expressed in OWL 2 RL using an informal elipsis notation. In implementing OWL 2 RL in RIF there are two ways of handling such rules. They can either be expressed as a set of recursive rules that traverse the RDF list structures at run-time or they can be regarded as templates that, for a given RDF input document, can be translated to a set of triple pattern rules as part of a preprocessing step. We define both options in this note.

Inconsistency rules indicate inconsistencies in the original RDF graph, they are expressed as first order rules which derive a propositional symbol false. We suggest a predicate symbol within the RIF namespace be used for this purpose.

Datatype rules these provide type checking and value equality/inequality checking for typed literals across a set of supported datatypes. The set of datatypes supported by RIF and OWL differ significantly. For those OWL 2 datatypes that are supported by RIF translation of the rules to RIF is largely straightforward.

3 Background OWL 2 RL

The OWL 2 RL profile [OWL 2 Profiles] is aimed at applications that require scalable reasoning in return for some restriction on expressive power. It defines a syntactic subset of OWL 2 that is amenable to implementation using rule-based technologies together with a partial axiomatization of the OWL 2 RDF-Based Semantics in the form of first-order implications that can be used as the basis for such an implementation.

For ontologies satisfying the syntactic constraints of the OWL 2 RL profile then a suitable rule-based implementation can provide sound and complete entailment checking and conjunctive query answering (so long as the query also meets the OWL 2 RL syntactic restrictions).

The purpose of this note is to provide a translation of the OWL 2 RL rules into RIF notation. The aim is that this translation be faithful to the OWL 2 RL semantics so that the follow theorem should hold:

Theorem 1. Let O1 and O2 be OWL 2 RL ontologies in both of which no URI is used for more than one type of entity (i.e., no URIs is used both as, say, a class and an individual), and where all axioms in O2 are assertions of the following form with a, a1, ..., an named individuals:

  • ClassAssertion( C a ) where C is a class
  • PropertyAssertion( P a1 a2 ) where P is an object property
  • PropertyAssertion( P a v ) where P is a data property
  • SameIndividual( a1 ... an )
  • DifferentIndividuals( a1 ... an )

Let R(O1) be either the fixed RIF rule set described in Appendix: OWL 2 RL ruleset - presentation syntax or the RIF rule set derived from O1 by the algorithm described in Appendix: OWL 2 RL to RIF translation.

Furthermore, let RDF(O1) and RDF(O2) be translations of O1 and O2, respectively, into RDF graphs as specified in the OWL 2 Mapping to RDF Graphs [OWL 2 RDF Mapping].

Then, O1 entails O2 under the OWL 2 RDF-Based semantics [OWL 2 RDF-Based Semantics] if and only if the RIF-RDF combination of R(O1) and RDF(O1) entails the generalized RDF graph RDF(O2) according to the notion of entailment for RIF-RDF combinations as defined in [RIF RDF and OWL Compatibility].

4 Analysis of OWL 2 RL rules

As noted above the OWL 2 RL rules fall into four categories which pose different issues for translation to RIF. We discuss each category in turn.

Note that throughout this section all rules given in RIF Core presentation syntax will assume the following prefix definitions: 

 Document(
   Prefix(rdf  http://www.w3.org/1999/02/22-rdf-syntax-ns#)
   Prefix(rdfs http://www.w3.org/2000/01/rdf-schema#)
   Prefix(owl  http://www.w3.org/2002/07/owl#)
   Prefix(xsd  http://www.w3.org/2001/XMLSchema#)
   Prefix(rif  http://www.w3.org/2007/rif#)
   Prefix(func http://www.w3.org/2007/rif-builtin-function#)
   Prefix(pred http://www.w3.org/2007/rif-builtin-predicate#)
   Prefix(dc   http://purl.org/dc/terms/)
   ...
 )

4.1 Triple pattern rules

The triple pattern rules take the form:

If then
T(s1, p1, o1)
...
T(sn, pn, on) 		T(sr1, pr1, or1)
...
T(srm, prm, orm)

where each argument to the T predicate may be a variable, an IRI or literal value.

Such rules can be expressed in the RIF Core presentation syntax as: 

 Group (
   Forall ?v11 ... ?v1o 
     ( sr1[pr1->or1] :- And( s1[p1->o1] ...  sn[pn->on] ))
   ...
   Forall ?vm1 ... ?vmo 
     ( srm[prm->orm] :- And( s1[p1->o1] ...  sn[pn->on] ))
 )

where ?vi1 ... ?vio are the variables which occur in the ith rule.

4.2 Inconsistency rules

A number of the OWL 2 RL rules detect inconsistencies in the original RDF graph. They express this by deriving a distinguished propositional symbol false.

For example:

If then
T(?p1, owl:propertyDisjointWith, ?p2)
T(?x, ?p1, ?y)
T(?x, ?p2, ?y) 		false

We translate such rules using a distinguished unary predicate rif:error(msg). If this predicate is derived then the original RDF graph is inconsistent under OWL 2 RL semantics.

Note: that the use of a unary rather than nullary predicate is arbitrary. We suggest the unary form to enable rules to report an explanation of the nature of the inconsistency by returning a diagnostic string as the argument to the error predicate.

Thus the above rule would be expressed in RIF Core as: 

  Forall ?p1 ?p2 ?x ?y ( 
    rif:error('disjoint property violation') :-  
      And( ?p1[owl:propertyDisjointWith->?p2] ?x[?p1->?y] ?x[?p2->?y] )
  )

or 

  Forall ?p1 ?p2 ?x ?y ?p1str ?p2Str ?xStr ?yStr ?msg( 
    rif:error(?msg) :-  
      And( ?p1[owl:propertyDisjointWith->?p2] ?x[?p1->?y] ?x[?p2->?y]
           _any-to-string(?p1 ?p1str), _any-to-string(?p2 ?p2Str), 
           _any-to-string(?x ?xStr), _any-to-string(?y ?yStr),
           ?msg = External ( func:concat('disjoint properties ' ?p1Str ' and ' ?p2Str 
                             ' both used between ' ?xStr ' and ' ?yStr) )

  Group (
   Forall ?x ?str (
     _any-to-string(?x ?str) :- ?str = External( xsd:string(?x) ))
   Forall ?x ?str (
     _any-to-string(?x ?str) :- External( pred:iri-to-string(?x ?str) ))
  )

4.3 List rules

A number of the OWL 2 RL rules involve processing OWL expressions which include RDF lists. Such rules are expressed in OWL 2 RL as templates which, for each possible list length, would correspond to a set of Triple Pattern rules.

There are two ways we can approach this in RIF. We can rewrite such rules as recursive rules that traverse the RDF list links or we can introduce the notion of a preprocessor which takes an OWL2 RL ontology in RDF syntax and translates it to a corresponding RIF rule set in which the templates rules have been instantiated for the lists that actually occur in the source ontology. This is possible because none of the rules is able to deduce new list entries for such lists within the syntactic constraints of OWL 2 RL.

The approach of using a fixed recursive rule set is appropriate to enable a single RIF OWL 2 RL ruleset to be published. However, the required rules violate the safe-rule checks for RIF Core and are not directly implementable by production rule engines. The translation approach yields rules which are more widely implementable and likely to perform better in practice.

We discuss the direct forms of the List Rules here and then describe in Appendix: OWL 2 RL to RIF translation the translation algorithm for the pre-processor approach.

The are several different patterns of List Rules in the OWL 2 RL ruleset, we discuss each group of rules in turn organized by the pattern involved.

4.3.1 Inconsistent pairs rules

These rules check whether any pair of entries from a list match a certain criterion and if they do an error is signaled (derivation of the false propositional symbol).

T(?yi, owl:sameAs, ?yj)
T(?x, rdf:type, owl:AllDifferent)
LIST[?x, ?y1, ..., ?yn] 		false for each 1 ≤ i < j ≤ n
T(?z, rdf:type, owl:AllDisjointProperties)
LIST[?z, ?p1, ..., ?pn]
T(?x, ?pi, ?y)
T(?x, ?pj, ?y) 		false for each 1 ≤ i < j ≤ n
T(?y, rdf:type, owl:AllDisjointClasses)
LIST[?y, ?c1, ..., ?cn]
T(?x, rdf:type, ?ci)
T(?x, rdf:type, ?cj) 		false for each 1 ≤ i < j ≤ n

These rules can be directly translated with the assistance of a utility predicate to select any element from an RDF list. 

  Forall ?x ?y ?l (
    rif:error('AllDifferent') :- And (
        ?l[rdf:type -> owl:AllDifferent]
        _member(?l ?x) _member(?l ?y) 
        ?x[owl:sameAs->?y] ) )

  Forall ?x ?y ?p1 ?p2 ?l (
    rif:error('AllDisjointProperties') :- And (
        ?l[rdf:type -> owl:AllDisjointProperties]
        _member(?l ?p1) _member(?l ?p2) 
        ?x[?p1->?y ?p2->?y]) )

  Forall ?x ?y ?c1 ?c2 ?l (
    rif:error('AllDisjointClasses') :- And (
        ?l[rdf:type -> owl:AllDisjointClasses]
        _member(?l ?c1) _member(?l ?c2) 
        ?x[rdf:type->?c1 rdf:type->?c2]) )

  Group (
   Forall ?list ?hd (
     _member(?list ?hd ) :- ?list[rdf:first -> ?hd] )

   Forall ?list ?tl ?x (
     _member( ?list ?x ) :- And( ?list[rdf:rest -> ?tl] _member(?tl ?x) ) )
  )

4.3.2 Property chain rule

This rule expands the list into a chain of properties that need to be checked in the rule body.

T(?sc, owl:propertyChain, ?x)
LIST[?x, ?p1, ..., ?pn]
T(?sc, rdfs:subPropertyOf, ?p)
T(?u1, ?p1, ?u2)
T(?u2, ?p2, ?u3)
...
T(?un, ?pn, ?un+1) 		T(?u1, ?p, ?un+1)

Which can be translated by the RIF Core rule set: 

  Forall ?p ?last ?pc ?start ?sc (
    ?start[?p->?last] :- And (
        ?sc[owl:propertyChain->?pc  rdfs:subPropertyOf->?p]
        _checkChain(?start ?pc ?last) ))

  Forall ?start ?pc ?last ?p ?tl (
    _checkChain(?start ?pc  ?last) :- And (
        ?pc[rdf:first->?p rdf:rest->?tl]
        ?start[?p->?next]
        _checkChain(?next ?tl ?last) ))

  Forall ?start (
    _checkChain(?start rdf:nil ?start) )

4.3.3 Haskey rule

This rule checks that two individuals are the same by virtual of having the same value for each of a list of key properties.

T(?c, owl:hasKey, ?u)
LIST[?u, ?p1, ..., ?pn]
T(?x, rdf:type, ?c)
T(?x, ?p1, ?z1)
...
T(?x, ?pn, ?zn)
T(?y, rdf:type, ?c)
T(?y, ?p1, ?z1)
...
T(?y, ?pn, ?zn) 		T(?x, owl:sameAs, ?y)

This can be translated by the RIF rule set: 

  Forall ?x ?y ?c ?u ?c (
    ?x[owl:sameAs->?y] :- And (
      ?c[owl:hasKey->?u]  ?x[rdf:type->?c]  ?y[rdf:type->?c]
      _sameKey(?u ?x ?y) ))

  Forall ?u ?x ?y (
    _sameKey(?u ?x ?y) :- And (
      ?u[rdf:first->?key rdf:rest->?tl]
      ?x[?key->?v] ?y[?key->?v]
      _sameKey(?tl ?x ?y) ))

  Forall ?x ?y (
    _sameKey(rdf:nil ?x ?y) )

Note that the last universal fact is not executable by a production rule engine.

4.3.4 Forward intersectionOf rule

This pattern involves a test for all members of a list.

T(?c, owl:intersectionOf, ?x)
LIST[?x, ?c1, ..., ?cn]
T(?y, rdf:type, ?c1)
T(?y, rdf:type, ?c2)
...
T(?y, rdf:type, ?cn) 		T(?y, rdf:type, ?c)

This can be translated by the RIF rule set: 

  Forall ?y ?c ?l (
    ?y[rdf:type->?c] :- And (
      ?c[owl:intersectionOf->?l]
      _allTypes(?l ?y) ))

  Forall ?l ?y ?ty ?tl (
    _allTypes(?l ?y) :- And (
      ?l[rdf:first->?ty rdf:rest->?tl]
      ?y[rdf:type->?ty]
      _allTypes(?tl ?y) ))

  Forall ?y (
    _allTypes(rdf:nil ?y) )

4.3.5 Simple member rules

This pattern involves a test for each member of a list.

T(?c, owl:unionOf, ?x)
LIST[?x, ?c1, ..., ?cn]
T(?y, rdf:type, ?ci) 		T(?y, rdf:type, ?c) for each 1 ≤ i ≤ n
T(?c, owl:oneOf, ?x)
LIST[?x, ?y1, ..., ?yn] 		T(?yi, rdf:type, ?c) for each 1 ≤ i ≤ n
T(?c, owl:intersectionOf, ?x)
LIST[?x, ?c1, ..., ?cn]
T(?y, rdf:type, ?c) 		T(?y, rdf:type, ?c1)
T(?y, rdf:type, ?c2)
...
T(?y, rdf:type, ?cn)
T(?c, owl:intersectionOf, ?x)
LIST[?x, ?c1, ..., ?cn] 		T(?c, rdfs:subClassOf, ?c1)
T(?c, rdfs:subClassOf, ?c2)
...
T(?c, rdfs:subClassOf, ?cn)
T(?c, owl:unionOf, ?x)
LIST[?x, ?c1, ..., ?cn] 		T(?c1, rdfs:subClassOf, ?c)
T(?c2, rdfs:subClassOf, ?c)
...
T(?cn, rdfs:subClassOf, ?c)

These can be translated by the RIF rule set: 

  Forall ?y ?c ?l ?ci (
    ?y[rdf:type->?c] :- And (
      ?c[owl:unionOf->?l]
      _member(?l ?ci)
      ?y[rdf:type->?ci] ))

  Forall ?yi ?c ?l (
    ?yi[rdf:type->?c] :- And (
      ?c[owl:oneOf->?l]
      _member(?l ?yi) ))

  Forall ?y ?c ?ci ?l (
    ?y[rdf:type->?ci] :- And (
      ?c[owl:intersectionOf->?l]
      _member(?l ?ci)
      ?y[rdf:type->?c] ))

  Forall ?c ?ci ?l (
    ?c[rdfs:subClassOf->?ci] :- And (
      ?c[owl:intersectionOf->?l]
      _member(?l ?ci) ))

  Forall ?c ?ci ?l (
    ?ci[rdfs:subClassOf->?c] :- And (
      ?c[owl:unionOf->?l]
      _member(?l ?ci) ))

where the member predicate was defined earlier.

4.4 Datatype rules

OWL 2 RL specifies four groups of rules to capture the semantics of supported datatypes. These are:

If then
true T(lt, rdf:type, dt) for each literal lt and each datatype dt supported in OWL 2 RL
such that the data value of lt is contained in the value space of dt
true T(lt1, owl:sameAs, lt2) for all literals lt1 and lt2 with the same data value
true T(lt1, owl:differentFrom, lt2) for all literals lt1 and lt2 with different data values
T(lt, rdf:type, dt) false for each literal lt and each datatype dt supported in OWL 2 RL
such that the data value of lt is not contained in the value space of dt

4.4.1 Datatypes supported

OWL 2 RL supports a set of datatypes which differs from that supported by RIF. The following table summarizes which of the OWL 2 RL datatypes are support by RIF.

Supported Subtype of supported type Not supported
rdf:text

xsd:decimal
xsd:integer
xsd:string
rdfs:Literal[*]

xsd:nonNegativeInteger
xsd:normalizedString
xsd:token
xsd:Name
xsd:NCName
xsd:NMTOKEN
xsd:ID
xsd:IDREF
xsd:ENTITY

xsd:hexBinary
xsd:base64Binary
xsd:anyURI
owl:dateTime
owl:real

[*] Note that while rdfs:Literal is not a RIF datatype, the relevant datatype entailments required for OWL2/RL can be derived using RIF rules with no additional support required.

4.4.2 Rules for supported datatypes

The RIF representation of the data type rules for supported datatypes is reasonably straightforward.

Type membership 

  Forall ?lt ( ?lt[rdf:type->rdf:text rdf:type->rdfs:Literal] :- External( pred:isText(?lt)) )
  Forall ?lt ( ?lt[rdf:type->xsd:decimal rdf:type->rdfs:Literal] :- External( pred:isDecimal(?lt)) )
  Forall ?lt ( ?lt[rdf:type->xsd:integer rdf:type->rdfs:Literal] :- External( pred:isInteger(?lt)) )
  Forall ?lt ( ?lt[rdf:type->xsd:string rdf:type->rdfs:Literal] :- External( pred:isString(?lt)) )

Equality 

  Forall ?l1 ?l2 ( ?l1[owl:sameAs->l2] ) :- ?l1 = ?l2 )

Inequality 

  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isText(?lt1)) External(pred:isNotText(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isNotText(?lt1)) External(pred:isText(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isText(?lt1)) External(pred:isText(?lt2)) 
    External(pred:numeric-not-equal( 0 
         External(func:compare( External(xsd:string(?lt1)) External(xsd:string(?lt2)) )) )) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isText(?lt1)) External(pred:isText(?lt2)) 
    External(pred:numeric-not-equal( 0 
         External(func:compare( External(func:lang(?lt1)) External(func:lang(?lt2)) )) )) ))

  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isDecimal(?lt1)) External(pred:isNotDecimal(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isNotDecimal(?lt1)) External(pred:isDecimal(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isDecimal(?lt1)) External(pred:isDecimal(?lt2)) 
    External(pred:numeric-not-equal( ?lt1 ?lt2 )) ))
    
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isInteger(?lt1)) External(pred:isNotInteger(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isNotInteger(?lt1)) External(pred:isInteger(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isInteger(?lt1)) External(pred:isInteger(?lt2)) 
    External(pred:numeric-not-equal( ?lt1 ?lt2 )) ))
    
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isString(?lt1)) External(pred:isNotString(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isNotString(?lt1)) External(pred:isString(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isString(?lt1)) External(pred:isString(?lt2)) 
    External(pred:numeric-not-equal( 0 
         External(func:compare( ?lt1 ?lt2 )) )) ))

Type checking 

  Forall ?lt ( 
    rif:error('datatype violation') :- And (
      ?lt[rdf:type->rif:text] External(pred:isNotText( ?lt )) ))
  Forall ?lt ( 
    rif:error('datatype violation') :- And (
      ?lt[rdf:type->xsd:decimal] External(pred:isNotDecimal( ?lt )) ))
  Forall ?lt ( 
    rif:error('datatype violation') - And (
      ?lt[rdf:type->xsd:integer] External(pred:isNotInteger( ?lt )) ))
  Forall ?lt ( 
    rif:error('datatype violation') :- And (
      ?lt[rdf:type->xsd:string] External(pred:isNotString( ?lt )) ))

4.4.3 Partial support for subtypes

OWL 2 RL includes support for several subtypes of xsd:string and one subtype of xsd:integer (viz. xsd:nonNegativeInteger).

Type membership and checking rules for these types can be implemented in RIF by coercion to the base type and an explicit check of the subrange using rule predicates.

Editor's Note: My reading of DTB is that the coercion functions should accept all subtypes of the base supported types, is that right?

As an example of this approach we illustrate the implementation of xsd:nonNegativeInteger. 

  Forall ?lt ( ?lt[rdf:type->xsd:nonNegativeInteger] :- isNonNegativeInteger( ?lt ) )

  Forall ?l1 ?l2 ( ?l1[owl:sameAs->l2] ) :- And (
    isNonNegativeInteger( ?l1 )
    isNonNegativeInteger( ?l2 )
    External(pred:numeric-equal(  External(func:xsd:integer(?l1))  
                                  External(func:xsd:integer(?l2)) )) ))

  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isNonNegativeInteger(?lt1)) External(pred:isNotNonNegativeInteger(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isNotNonNegativeInteger(?lt1)) External(pred:isNonNegativeInteger(?lt2)) ))
  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :- And (
    External(pred:isNonNegativeInteger(?lt1)) External(pred:isNonNegativeInteger(?lt2)) 
    External(pred:numeric-not-equal(  External(func:xsd:integer(?l1))  
                                      External(func:xsd:integer(?l2)) )) ))

  Forall ?lt ( 
    rif:error('datatype violation') - And (
      ?lt[rdf:type->xsd:nonNegativeInteger] External(pred:isNotNonNegativeInteger( ?lt )) ))

  Forall ?lt (
    isNonNegativeInteger( ?lt ) :-  And (
      External(func:isInteger( ?lt ))
      External(pred:numeric-greater-than-or-equal( 
             External(func:xsd:integer( ?lt )) 0 )) ))

  Forall ?lt (
    isNotNonNegativeInteger( ?lt ) :- And (
      External(func:isInteger( ?lt ))
      External(pred:numeric-less-than( 
             External(func:xsd:integer( ?lt )) 0 )) ))

  Forall ?lt (
    isNotNonNegativeInteger( ?lt ) :- 
      External(func:isNotInteger( ?lt )) )

4.4.4 Datatype rules with extended builtins

Whilst the above datatype rules are sufficient, at least for the supported datatypes, they could be simpler. Predicates for membership/non-membership and value equality/non-equality which spanned all literal datatypes would both simplify the above rules and enable them to automatically support any additional datatypes supported by the consuming RIF implementation.

In that case the entire datatype rule subset would look like: 

  Forall ?lt ?dt ( ?lt[rdf:type->?dt rdf:type->rdfs:Literal] :- External(pred:isType(?lt ?dt)) )

  Forall ?l1 ?l2 ( ?l1[owl:sameAs->l2] ) :- External(pred:isLiteralEqual(?l1 ?l2)) )

  Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :-
                                       External(pred:isLiteralNotEqual(?l1 ?l2)) )

  Forall ?lt ?dt ( 
    rif:error('datatype violation') - And (
      ?lt[rdf:type->dt] External(pred:isNotType( ?lt ?dt )) ))

5 References

[OWL 2 Profiles]
OWL 2 Web Ontology Language Profiles, Grau et al eds, 2008.
[OWL 2 RDF Mapping]
OWL 2 Web Ontology Language: Mapping to RDF Graphs. Bernardo Cuenca Grau and Boris Motik, eds., 2008.
[OWL 2 Semantics]
OWL 2 Web Ontology Language: Model-Theoretic Semantics. Bernardo Cuenca Grau and Boris Motik, eds., 2008.
[RIF RDF and OWL Compatibility]
RIF RDF and OWL Compatibility. Jos de Bruijn ed, 2008.

6 Appendix: OWL 2 RL ruleset - presentation syntax

In this appendix we provide a RIF Core presentation syntax translation of the complete OWL 2 RL ruleset. We divide these rules into three documents - the simple triple rules (mechanically translated from the OWL 2 RL rule format), the List rules and the datatype rules. For latter we currently present the short version which assumes additional builtins as described in Datatype rules with extended builtins.

Editor's Note: The manual rules (and indeed the manually written mechanical translator) may include syntactic errors, the intent is to verify them once we have a working PS-to-XML translator.

Editor's Note: Note that the rules here are a direct translation of the OWL2/RL rules from [OWL 2 Profiles] into RIF. At the current time some rules such as those involving owl:allDisjoint are not consistent with the current RDF serialization for OWL2 but we have chosen to track the [OWL 2 Profiles] document rather than second guess future changes.

Simple triple rules 

Document (
  Prefix(rdf  http://www.w3.org/1999/02/22-rdf-syntax-ns#)
  Prefix(rdfs http://www.w3.org/2000/01/rdf-schema#)
  Prefix(owl  http://www.w3.org/2002/07/owl#)
  Prefix(xsd  http://www.w3.org/2001/XMLSchema#)
  Prefix(rif  http://www.w3.org/2007/rif#)
  Prefix(func http://www.w3.org/2007/rif-builtin-function#)
  Prefix(pred http://www.w3.org/2007/rif-builtin-predicate#)
  Prefix(dc   http://purl.org/dc/terms/)
  Group (

Forall ?p ?o ?s (
   ?s[owl:sameAs->?s] :- ?s[?p->?o] )

Forall ?p ?o ?s (
   ?p[owl:sameAs->?p] :- ?s[?p->?o] )

Forall ?p ?o ?s (
   ?o[owl:sameAs->?o] :- ?s[?p->?o] )

Forall ?x ?y (
   ?y[owl:sameAs->?x] :- ?x[owl:sameAs->?y] )

Forall ?x ?z ?y (
   ?x[owl:sameAs->?z] :- And(
       ?x[owl:sameAs->?y]
       ?y[owl:sameAs->?z]  ))

Forall ?p ?o ?s ?sp (
   ?sp[?p->?o] :- And(
       ?s[owl:sameAs->?sp]
       ?s[?p->?o]  ))

Forall ?p ?o ?pp ?s (
   ?s[?pp->?o] :- And(
       ?p[owl:sameAs->?pp]
       ?s[?p->?o]  ))

Forall ?p ?o ?s ?op (
   ?s[?p->?op] :- And(
       ?o[owl:sameAs->?op]
       ?s[?p->?o]  ))

Forall ?x ?y (
   rif:error("inconsistent") :- And(
       ?x[owl:sameAs->?y]
       ?x[owl:differentFrom->?y]  ))

Forall ?p ?c ?x ?y (
   ?x[rdf:type->?c] :- And(
       ?p[rdfs:domain->?c]
       ?x[?p->?y]  ))

Forall ?p ?c ?x ?y (
   ?y[rdf:type->?c] :- And(
       ?p[rdfs:range->?c]
       ?x[?p->?y]  ))

Forall ?p ?y2 ?x ?y1 (
   ?y1[owl:sameAs->?y2] :- And(
       ?p[rdf:type->owl:FunctionalProperty]
       ?x[?p->?y1]
       ?x[?p->?y2]  ))

Forall ?p ?x1 ?x2 ?y (
   ?x1[owl:sameAs->?x2] :- And(
       ?p[rdf:type->owl:InverseFunctionalProperty]
       ?x1[?p->?y]
       ?x2[?p->?y]  ))

Forall ?p ?x ?z ?y (
   ?x[?p->?x] :- And(
       ?p[rdf:type->owl:ReflexiveProperty]
       ?x[?y->?z]  ))

Forall ?p ?x ?z ?y (
   ?y[?p->?y] :- And(
       ?p[rdf:type->owl:ReflexiveProperty]
       ?x[?y->?z]  ))

Forall ?p ?x ?z ?y (
   ?z[?p->?z] :- And(
       ?p[rdf:type->owl:ReflexiveProperty]
       ?x[?y->?z]  ))

Forall ?p ?x (
   rif:error("inconsistent") :- And(
       ?p[rdf:type->owl:IrreflexiveProperty]
       ?x[?p->?x]  ))

Forall ?p ?x ?y (
   ?y[?p->?x] :- And(
       ?p[rdf:type->owl:SymmetricProperty]
       ?x[?p->?y]  ))

Forall ?p ?x ?y (
   rif:error("inconsistent") :- And(
       ?p[rdf:type->owl:AsymmetricProperty]
       ?x[?p->?y]
       ?y[?p->?x]  ))

Forall ?p ?x ?z ?y (
   ?x[?p->?z] :- And(
       ?p[rdf:type->owl:TransitiveProperty]
       ?x[?p->?y]
       ?y[?p->?z]  ))

Forall ?x ?y ?p2 ?p1 (
   ?x[?p2->?y] :- And(
       ?p1[rdfs:subPropertyOf->?p2]
       ?x[?p1->?y]  ))

Forall ?x ?y ?p2 ?p1 (
   ?x[?p2->?y] :- And(
       ?p1[owl:equivalentProperty->?p2]
       ?x[?p1->?y]  ))

Forall ?x ?y ?p2 ?p1 (
   ?x[?p1->?y] :- And(
       ?p1[owl:equivalentProperty->?p2]
       ?x[?p2->?y]  ))

Forall ?x ?y ?p2 ?p1 (
   rif:error("inconsistent") :- And(
       ?p1[owl:propertyDisjointWith->?p2]
       ?x[?p1->?y]
       ?x[?p2->?y]  ))

Forall ?x ?y ?p2 ?p1 (
   ?y[?p2->?x] :- And(
       ?p1[owl:inverseOf->?p2]
       ?x[?p1->?y]  ))

Forall ?x ?y ?p2 ?p1 (
   ?y[?p1->?x] :- And(
       ?p1[owl:inverseOf->?p2]
       ?x[?p2->?y]  ))

Forall ?p ?v ?u ?x ?y (
   ?u[rdf:type->?x] :- And(
       ?x[owl:someValuesFrom->?y]
       ?x[owl:onProperty->?p]
       ?u[?p->?v]
       ?v[rdf:type->?y]  ))

Forall ?p ?v ?u ?x ?y (
   ?v[rdf:type->?y] :- And(
       ?x[owl:allValuesFrom->?y]
       ?x[owl:onProperty->?p]
       ?u[rdf:type->?x]
       ?u[?p->?v]  ))

Forall ?p ?u ?x ?y (
   ?u[?p->?y] :- And(
       ?x[owl:hasValue->?y]
       ?x[owl:onProperty->?p]
       ?u[rdf:type->?x]  ))

Forall ?p ?u ?x ?y (
   ?u[rdf:type->?x] :- And(
       ?x[owl:hasValue->?y]
       ?x[owl:onProperty->?p]
       ?u[?p->?y]  ))

Forall ?p ?u ?x ?y (
   rif:error("inconsistent") :- And(
       ?x[owl:maxCardinality->0]
       ?x[owl:onProperty->?p]
       ?u[?p->?y]
       ?u[rdf:type->?x]  ))

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

Forall ?x ?c1 ?c2 (
   ?x[rdf:type->?c2] :- And(
       ?c1[rdfs:subClassOf->?c2]
       ?x[rdf:type->?c1]  ))

Forall ?x ?c1 ?c2 (
   ?x[rdf:type->?c2] :- And(
       ?c1[owl:equivalentClass->?c2]
       ?x[rdf:type->?c1]  ))

Forall ?x ?c1 ?c2 (
   ?x[rdf:type->?c1] :- And(
       ?c1[owl:equivalentClass->?c2]
       ?x[rdf:type->?c2]  ))

Forall ?x ?c1 ?c2 (
   rif:error("inconsistent") :- And(
       ?c1[owl:disjointWith->?c2]
       ?x[rdf:type->?c1]
       ?x[rdf:type->?c2]  ))

Forall ?c (
   ?c[rdfs:subClassOf->?c] :- ?c[rdf:type->owl:Class] )

Forall ?c (
   ?c[owl:equivalentClass->?c] :- ?c[rdf:type->owl:Class] )

Forall ?c1 ?c2 ?c3 (
   ?c1[rdfs:subClassOf->?c3] :- And(
       ?c1[rdfs:subClassOf->?c2]
       ?c2[rdfs:subClassOf->?c3]  ))

Forall ?c1 ?c2 (
   ?c1[rdfs:subClassOf->?c2] :- ?c1[owl:equivalentClass->?c2] )

Forall ?c1 ?c2 (
   ?c2[rdfs:subClassOf->?c1] :- ?c1[owl:equivalentClass->?c2] )

Forall ?p (
   ?p[rdfs:subPropertyOf->?p] :- ?p[rdf:type->owl:ObjectProperty] )

Forall ?p (
   ?p[owl:equivalentProperty->?p] :- ?p[rdf:type->owl:ObjectProperty] )

Forall ?p (
   ?p[rdfs:subPropertyOf->?p] :- ?p[rdf:type->owl:DatatypeProperty] )

Forall ?p (
   ?p[owl:equivalentProperty->?p] :- ?p[rdf:type->owl:DatatypeProperty] )

Forall ?p3 ?p2 ?p1 (
   ?p1[rdfs:subPropertyOf->?p3] :- And(
       ?p1[rdfs:subPropertyOf->?p2]
       ?p2[rdfs:subPropertyOf->?p3]  ))

Forall ?p2 ?p1 (
   ?p1[rdfs:subPropertyOf->?p2] :- ?p1[owl:equivalentProperty->?p2] )

Forall ?p2 ?p1 (
   ?p2[rdfs:subPropertyOf->?p1] :- ?p1[owl:equivalentProperty->?p2] )

Forall ?p ?c1 ?c2 (
   ?p[rdfs:domain->?c2] :- And(
       ?p[rdfs:domain->?c1]
       ?c1[rdfs:subClassOf->?c2]  ))

Forall ?c ?p2 ?p1 (
   ?p1[rdfs:domain->?c] :- And(
       ?p2[rdfs:domain->?c]
       ?p1[rdfs:subPropertyOf->?p2]  ))

Forall ?p ?c1 ?c2 (
   ?p[rdfs:range->?c2] :- And(
       ?p[rdfs:range->?c1]
       ?c1[rdfs:subClassOf->?c2]  ))

Forall ?c ?p2 ?p1 (
   ?p1[rdfs:range->?c] :- And(
       ?p2[rdfs:range->?c]
       ?p1[rdfs:subPropertyOf->?p2]  ))

Forall ?c1 ?c2 ?i ?p2 ?p1 (
   ?c1[rdfs:subClassOf->?c2] :- And(
       ?c1[owl:hasValue->?i]
       ?c1[owl:onProperty->?p1]
       ?c2[owl:hasValue->?i]
       ?c2[owl:onProperty->?p2]
       ?p1[rdfs:subPropertyOf->?p2]  ))

Forall ?p ?y2 ?c1 ?c2 ?y1 (
   ?c1[rdfs:subClassOf->?c2] :- And(
       ?c1[owl:someValuesFrom->?y1]
       ?c1[owl:onProperty->?p]
       ?c2[owl:someValuesFrom->?y2]
       ?c2[owl:onProperty->?p]
       ?y1[rdfs:subClassOf->?y2]  ))

Forall ?c1 ?c2 ?y ?p2 ?p1 (
   ?c1[rdfs:subClassOf->?c2] :- And(
       ?c1[owl:someValuesFrom->?y]
       ?c1[owl:onProperty->?p1]
       ?c2[owl:someValuesFrom->?y]
       ?c2[owl:onProperty->?p2]
       ?p1[rdfs:subPropertyOf->?p2]  ))

Forall ?p ?y2 ?c1 ?c2 ?y1 (
   ?c1[rdfs:subClassOf->?c2] :- And(
       ?c1[owl:allValuesFrom->?y1]
       ?c1[owl:onProperty->?p]
       ?c2[owl:allValuesFrom->?y2]
       ?c2[owl:onProperty->?p]
       ?y1[rdfs:subClassOf->?y2]  ))

Forall ?c1 ?c2 ?y ?p2 ?p1 (
   ?c2[rdfs:subClassOf->?c1] :- And(
       ?c1[owl:allValuesFrom->?y]
       ?c1[owl:onProperty->?p1]
       ?c2[owl:allValuesFrom->?y]
       ?c2[owl:onProperty->?p2]
       ?p1[rdfs:subPropertyOf->?p2]  ))

 )
)

List rules 

Document (
  Prefix(rdf  http://www.w3.org/1999/02/22-rdf-syntax-ns#)
  Prefix(rdfs http://www.w3.org/2000/01/rdf-schema#)
  Prefix(owl  http://www.w3.org/2002/07/owl#)
  Prefix(xsd  http://www.w3.org/2001/XMLSchema#)
  Prefix(rif  http://www.w3.org/2007/rif#)
  Prefix(func http://www.w3.org/2007/rif-builtin-function#)
  Prefix(pred http://www.w3.org/2007/rif-builtin-predicate#)
  Prefix(dc   http://purl.org/dc/terms/)
   Group (

 Forall ?x ?y ?l (
   rif:error('AllDifferent') :- And (
       ?l[rdf:type -> owl:AllDifferent]
       _member(?l ?x) _member(?l ?y) 
       ?x[owl:sameAs->?y] ) )

 Forall ?x ?y ?p1 ?p2 ?l (
   rif:error('AllDisjointProperties') :- And (
       ?l[rdf:type -> owl:AllDisjointProperties]
       _member(?l ?p1) _member(?l ?p2) 
       ?x[?p1->?y ?p2->?y]) )

 Forall ?x ?y ?c1 ?c2 ?l (
   rif:error('AllDisjointClasses') :- And (
       ?l[rdf:type -> owl:AllDisjointClasses]
       _member(?l ?c1) _member(?l ?c2) 
       ?x[rdf:type->?c1 rdf:type->?c2]) )

  Forall ?list ?hd (
    _member(?list ?hd ) :- ?list[rdf:first -> ?hd] )

  Forall ?list ?tl ?x (
    _member( ?list ?x ) :- And( ?list[rdf:rest -> ?tl] _member(?tl ?x) ) )

 Forall ?p ?last ?pc ?start ?sc (
   ?start[?p->?last] :- And (
       ?sc[owl:propertyChain->?pc  rdfs:subPropertyOf->?p]
       _checkChain(?start ?pc ?last) ))

 Forall ?start ?pc ?last ?p ?tl (
   _checkChain(?start ?pc  ?last) :- And (
       ?pc[rdf:first->?p rdf:rest->?tl]
       ?start[?p->?next]
       _checkChain(?next ?tl ?last) ))

 Forall ?start (
   _checkChain(?start rdf:nil ?start) )

 Forall ?x ?y ?c ?u (
   ?x[owl:sameAs->?y] :- And (
     ?c[owl:hasKey->?u]  ?x[rdf:type->?c]  ?y[rdf:type->?c]
     _sameKey(?u ?x ?y) ))

 Forall ?u ?x ?y (
   _sameKey(?u ?x ?y) :- And (
     ?u[rdf:first->?key rdf:rest->?tl]
     ?x[?key->?v] ?y[?key->?v]
     _sameKey(?tl ?x ?y) ))

 Forall ?x ?y (
   _sameKey(rdf:nil ?x ?y) )

 Forall ?y ?c ?l (
   ?y[rdf:type->?c] :- And (
     ?c[owl:intersectionOf->?l]
     _allTypes(?l ?y) ))

 Forall ?l ?y ?ty ?tl (
   _allTypes(?l ?y) :- And (
     ?l[rdf:first->?ty rdf:rest->?tl]
     ?y[rdf:type->?ty]
     _allTypes(?tl ?y) ))

 Forall ?y (
   _allTypes(rdf:nil ?y) )

 Forall ?y ?c ?l ?ci (
   ?y[rdf:type->?c] :- And (
     ?c[owl:unionOf->?l]
     _member(?l ?ci)
     ?y[rdf:type->?ci] ))

 Forall ?yi ?c ?l (
   ?yi[rdf:type->?c] :- And (
     ?c[owl:oneOf->?l]
     _member(?l ?yi) ))

 Forall ?y ?c ?ci ?l (
   ?y[rdf:type->?ci] :- And (
     ?c[owl:intersectionOf->?l]
     _member(?l ?ci)
     ?y[rdf:type->?c] ))

 Forall ?c ?ci ?l (
   ?c[rdfs:subClassOf->?ci] :- And (
     ?c[owl:intersectionOf->?l]
     _member(?l ?ci) ))

 Forall ?c ?ci ?l (
   ?ci[rdfs:subClassOf->?c] :- And (
     ?c[owl:unionOf->?l]
     _member(?l ?ci) ))

 )
)


Datatype rules 

Document (
  Prefix(rdf  http://www.w3.org/1999/02/22-rdf-syntax-ns#)
  Prefix(rdfs http://www.w3.org/2000/01/rdf-schema#)
  Prefix(owl  http://www.w3.org/2002/07/owl#)
  Prefix(xsd  http://www.w3.org/2001/XMLSchema#)
  Prefix(rif  http://www.w3.org/2007/rif#)
  Prefix(func http://www.w3.org/2007/rif-builtin-function#)
  Prefix(pred http://www.w3.org/2007/rif-builtin-predicate#)
  Prefix(dc   http://purl.org/dc/terms/)
 Group (

 Forall ?lt ?dt ( ?lt[rdf:type->?dt rdf:type->rdfs:Literal] :- External(pred:isType(?lt ?dt)) )

 Forall ?l1 ?l2 ( ?l1[owl:sameAs->l2] ) :- External(pred:isLiteralEqual(?l1 ?l2)) )

 Forall ?lt1 ?lt2 ( ?lt1[owl:differentFrom->?lt2] :-
                                      External(pred:isLiteralNotEqual(?l1 ?l2)) )

 Forall ?lt ?dt ( 
   rif:error('datatype violation') :- And (
     ?lt[rdf:type->dt] External(pred:isNotType( ?lt ?dt )) ))

 )
)

7 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 includes rules which do not meet strict safeness criteria and so are not executable by a forward chaining engine such as a production rule system.

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) ) ∪ datatypeRules( RDF(O) )

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

7.1 FixedRules

The FixedRule ruleset comprises the following rules: 

Forall ?p ?o ?s (
   ?s[owl:sameAs->?s] :- ?s[?p->?o] )

Forall ?p ?o ?s (
   ?p[owl:sameAs->?p] :- ?s[?p->?o] )

Forall ?p ?o ?s (
   ?o[owl:sameAs->?o] :- ?s[?p->?o] )

Forall ?x ?y (
   ?y[owl:sameAs->?x] :- ?x[owl:sameAs->?y] )

Forall ?x ?z ?y (
   ?x[owl:sameAs->?z] :- And(
       ?x[owl:sameAs->?y]
       ?y[owl:sameAs->?z]  ))

Forall ?p ?o ?s ?sp (
   ?sp[?p->?o] :- And(
       ?s[owl:sameAs->?sp]
       ?s[?p->?o]  ))

Forall ?p ?o ?pp ?s (
   ?s[?pp->?o] :- And(
       ?p[owl:sameAs->?pp]
       ?s[?p->?o]  ))

Forall ?p ?o ?s ?op (
   ?s[?p->?op] :- And(
       ?o[owl:sameAs->?op]
       ?s[?p->?o]  ))

Forall ?x ?y (
   rif:error("inconsistent") :- And(
       ?x[owl:sameAs->?y]
       ?x[owl:differentFrom->?y]  ))

Forall ?x ?c1 ?c2 (
   ?x[rdf:type->?c2] :- And(
       ?c1[rdfs:subClassOf->?c2]
       ?x[rdf:type->?c1]  ))

Forall ?x ?c1 ?c2 (
   ?x[rdf:type->?c2] :- And(
       ?c1[owl:equivalentClass->?c2]
       ?x[rdf:type->?c1]  ))

Forall ?x ?c1 ?c2 (
   ?x[rdf:type->?c1] :- And(
       ?c1[owl:equivalentClass->?c2]
       ?x[rdf:type->?c2]  ))

Forall ?x ?c1 ?c2 (
   rif:error("inconsistent") :- And(
       ?c1[owl:disjointWith->?c2]
       ?x[rdf:type->?c1]
       ?x[rdf:type->?c2]  ))

Forall ?c (
   ?c[rdfs:subClassOf->?c] :- ?c[rdf:type->owl:Class] )

Forall ?c (
   ?c[owl:equivalentClass->?c] :- ?c[rdf:type->owl:Class] )

Forall ?c1 ?c2 ?c3 (
   ?c1[rdfs:subClassOf->?c3] :- And(
       ?c1[rdfs:subClassOf->?c2]
       ?c2[rdfs:subClassOf->?c3]  ))

Forall ?c1 ?c2 (
   ?c1[rdfs:subClassOf->?c2] :- ?c1[owl:equivalentClass->?c2] )

Forall ?c1 ?c2 (
   ?c2[rdfs:subClassOf->?c1] :- ?c1[owl:equivalentClass->?c2] )

Forall ?p (
   ?p[rdfs:subPropertyOf->?p] :- ?p[rdf:type->owl:ObjectProperty] )

Forall ?p (
   ?p[owl:equivalentProperty->?p] :- ?p[rdf:type->owl:ObjectProperty] )

Forall ?p (
   ?p[rdfs:subPropertyOf->?p] :- ?p[rdf:type->owl:DatatypeProperty] )

Forall ?p (
   ?p[owl:equivalentProperty->?p] :- ?p[rdf:type->owl:DatatypeProperty] )

Forall ?p3 ?p2 ?p1 (
   ?p1[rdfs:subPropertyOf->?p3] :- And(
       ?p1[rdfs:subPropertyOf->?p2]
       ?p2[rdfs:subPropertyOf->?p3]  ))

Forall ?p2 ?p1 (
   ?p1[rdfs:subPropertyOf->?p2] :- ?p1[owl:equivalentProperty->?p2] )

Forall ?p2 ?p1 (
   ?p2[rdfs:subPropertyOf->?p1] :- ?p1[owl:equivalentProperty->?p2] )

Forall ?p ?c ?x ?y (
   ?x[rdf:type->?c] :- And(
       ?p[rdfs:domain->?c]
       ?x[?p->?y]  ))

Forall ?p ?c ?x ?y (
   ?y[rdf:type->?c] :- And(
       ?p[rdfs:range->?c]
       ?x[?p->?y]  ))

Forall ?p ?c1 ?c2 (
   ?p[rdfs:domain->?c2] :- And(
       ?p[rdfs:domain->?c1]
       ?c1[rdfs:subClassOf->?c2]  ))

Forall ?c ?p2 ?p1 (
   ?p1[rdfs:domain->?c] :- And(
       ?p2[rdfs:domain->?c]
       ?p1[rdfs:subPropertyOf->?p2]  ))

Forall ?p ?c1 ?c2 (
   ?p[rdfs:range->?c2] :- And(
       ?p[rdfs:range->?c1]
       ?c1[rdfs:subClassOf->?c2]  ))

Forall ?c ?p2 ?p1 (
   ?p1[rdfs:range->?c] :- And(
       ?p2[rdfs:range->?c]
       ?p1[rdfs:subPropertyOf->?p2]  ))

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

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]  ))

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. 
$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.

The templateRule algorithm is defined using this notation by the following set of pattern/template pairs.

Pattern Template
(?p rdf:type owl:FunctionalProperty) 
Forall ?y2 ?x ?y1 (
   ?y1[owl:sameAs->?y2] :- And(
       ?x[?p->?y1]
       ?x[?p->?y2]  ))
(?p rdf:type owl:InverseFunctionalProperty]) 
Forall ?x1 ?x2 ?y (
   ?x1[owl:sameAs->?x2] :- And(
       ?x1[?p->?y]
       ?x2[?p->?y]  ))
(?p rdf:type owl:ReflexiveProperty) 
Forall ?x ?z ?y (
   ?x[?p->?x] :- And(
       ?x[?y->?z]  ))

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

Forall ?x ?z ?y (
   ?z[?p->?z] :- And(
       ?x[?y->?z]  ))
(?p rdf:type owl:IrreflexiveProperty) 
Forall ?x (
   rif:error("inconsistent") :- And(
       ?x[?p->?x]  ))
(?p rdf:type owl:SymmetricProperty) 
Forall ?x ?y (
   ?y[?p->?x] :- And(
       ?x[?p->?y]  ))
(?p rdf:type owl:AsymmetricProperty) 
Forall ?x ?y (
   rif:error("inconsistent") :- And(
       ?x[?p->?y]
       ?y[?p->?x]  ))
(?p rdf:type owl:TransitiveProperty) 
Forall ?x ?z ?y (
   ?x[?p->?z] :- And(
       ?x[?p->?y]
       ?y[?p->?z]  ))
(?p1 rdfs:subPropertyOf ?p2) 
Forall ?x ?y (
   ?x[?p2->?y] :- And(
       ?x[?p1->?y]  ))
(?p1 owl:equivalentProperty ?p2) 
Forall ?x ?y (
   ?x[?p2->?y] :- And(
       ?x[?p1->?y]  ))

Forall ?x ?y (
   ?x[?p1->?y] :- And(
       ?x[?p2->?y]  ))
(?p1 owl:propertyDisjointWith ?p2) 
Forall ?x ?y (
   rif:error("inconsistent") :- And(
       ?x[?p1->?y]
       ?x[?p2->?y]  ))
(?p1 owl:inverseOf ?p2) 
Forall ?x ?y (
   ?y[?p2->?x] :- And(
       ?x[?p1->?y]  ))

Forall ?x ?y (
   ?y[?p1->?x] :- And(
       ?x[?p2->?y]  ))
(?x owl:someValuesFrom ?y)
(?x owl:onProperty ?p) 
Forall ?v ?u (
   ?u[rdf:type->?x] :- And(
       ?u[?p->?v]
       ?v[rdf:type->?y]  ))
(?x owl:allValuesFrom ?y)
(?x owl:onProperty ?p) 
Forall ?v ?u (
   ?v[rdf:type->?y] :- And(
       ?u[rdf:type->?x]
       ?u[?p->?v]  ))
(?x owl:hasValue ?y)
(?x owl:onProperty ?p) 
Forall ?u (
   ?u[?p->?y] :- And(
       ?u[rdf:type->?x]  ))

Forall ?u (
   ?u[rdf:type->?x] :- And(
       ?u[?p->?y]  ))
(?x owl:maxCardinality 0)
(?x owl:onProperty ?p) 
Forall ?u ?y (
   rif:error("inconsistent") :- And(
       ?u[?p->?y]
       ?u[rdf:type->?x]  ))
(?x owl:maxCardinality 1)
(?x owl:onProperty ?p) 
Forall ?y2 ?u ?y1 (
   ?y1[owl:sameAs->?y2] :- And(
       ?u[?p->?y1]
       ?u[?p->?y2]
       ?u[rdf:type->?x]  ))
(?c1 owl:hasValue ?i)
(?c1 owl:onProperty ?p1)
(?c2 owl:hasValue ?i)
(?c2 owl:onProperty ?p2) 
Forall (
   ?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) 
Forall  (
   ?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) 
Forall (
   ?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) 
Forall (
   ?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) 
Forall  (
   ?c2[rdfs:subClassOf->?c1] :- And(
       ?p1[rdfs:subPropertyOf->?p2]  ))
(?l rdf:type owl:AllDifferent) 
for(?x in ?l) {
 for(?y in ?l) {
   {$
 Forall  (
   rif:error('AllDifferent') :- And (
       ?x[owl:sameAs->?y] ) )
   $}
 }
}
(?l rdf:type owl:AllDisjointProperties) 
for(?x in ?l) {
 for(?y in ?l) {
   {$
 Forall ?p1 ?p2 (
   rif:error('AllDisjointProperties') :- And (
       ?x[?p1->?y ?p2->?y]) )
   $}
 }
}
(?l rdf:type owl:AllDisjointClasses) 
for(?x in ?l) {
 for(?y in ?l) {
   {$
 Forall ?c1 ?c2 (
   rif:error('AllDisjointClasses') :- And (
       ?x[rdf:type->?c1 rdf:type->?c2]) )
    $}
 }
}
(?sc owl:propertyChain ?pc)
(?sc rdfs:subPropertyOf ?p) 
{$
 Forall ?u0 ?u$length(?pc)$ (
   ?start[?p->?last] :- And (
$}
for(?next in ?sc) {
  {$
    ?u$i$[?next->?u$i+1$]
  $}
}
{$ )) $}
(?c owl:hasKey ?u) 
{$
 Forall ?x ?y (
   ?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) 
{$
 Forall ?y (
   ?y[rdf:type->?c] :- And (
$}
for(?ty in ?l) {
 {$
     ?y[rdf:type->?ty]
 $}      
}    
{$ )) $}
(?c owl:unionOf ?l) 
for(?ci in ?l) {
 {$
   Forall ?y (
     ?y[rdf:type->?c] :- And (
       ?y[rdf:type->?ci] ))
 $}
}
(?c owl:oneOf ?l) 
for(?yi in ?l) {
 {$
   Forall ( ?yi[rdf:type->?c] )
 $}
}
(?c owl:intersectionOf ?l) 
for(?ci in ?l) {
 {$
   Forall ?y (
     ?y[rdf:type->?ci] :- And (
       ?y[rdf:type->?c] ))
       
   Forall( ?c[rdfs:subClassOf->?ci] )
 $}
}
(?c owl:unionOf ?l) 
for(?ci in ?l) {
 {$
   Forall ( ?ci[rdfs:subClassOf->?c] )
 $}
}

7.3 datatypeRules algorithm

The set of datatype rules for RDF(O) is obtained as follows:

1. Extract literals the set of all distinct literal values which occur in the object position of all triples in RDF(O).

2. Emit the fixed rule: 

 Forall ?lt ?dt ( 
   rif:error('datatype violation') :- And (
     ?lt[rdf:type->dt] External(pred:isNotType( ?lt ?dt )) ))

3. For each element ?lt in literals determine its datatype ?dt and emit the following fact: 

 ?lt[rdf:type->?dt rdf:type->rdfs:Literal]

4. For each pair of elements ?l1 and ?l2 from literals X literals emit the following facts:
If ?l1 equals ?l2 emit: 

 ?l1[owl:sameAs->l2]

If ?l1 does not equal ?l2 emit: 

 ?lt1[owl:differentFrom->?lt2]

N.B. This is a demonstration that the rewrite to safe RIF Core rules is possible. This is not a scalable solution since this algorithm will generate a ruleset which scales quadratically in the size of literals and in practical ontologies there are large numbers of literals.

Practical implementations are expected to not explicitly generate these facts but to rewrite each relevant mention of owl:sameAs and owl:differentFrom in the previous rule sets with embedded calls to pred:isLiteralEqual and pred:isLiteralNotEqual. At this stage a scalable version of the algorithm is left as an exercise for the reader.

Retrieved from "http://www.w3.org/2005/rules/wiki/OWLRL"