OWL 2 reasoning with SWRL rules

Question

I'm trying to use the HermiT reasoner to compute inferences for an ontology which contains a set of OWL axioms and a SWRL rule:

Ontology(
  ClassAssertion( :Student :Bob )
  ClassAssertion( :Professor :DrBoffin )
  ClassAssertion( :University :UF )
  ObjectPropertyAssertion( :supervises :DrBoffin :Bob )
  ObjectPropertyAssertion( :worksAt :DrBoffin :UF )

  EquivalentClasses( :Student ObjectHasSelf( :r1 ))
  EquivalentClasses(
    ObjectHasSelf( :r2 )
    ObjectSomeValuesFrom( :worksAt :University ))
  SubObjectPropertyOf(
    ObjectPropertyChain( :r2 :supervises :r1 ) :professorOf )

  DLSafeRule(Body(ObjectPropertyAtom( :professorOf Variable( ?x ) Variable( ?y )))
             Head(ObjectPropertyAtom( :instructorOf Variable( ?x ) Variable( ?y ))))
)

Basically, the OWL part is trying to express such a rule:

worksAt(x, y), University(y), supervises(x, z), Student(z) -> professorOf(x, z)

using property chain and rolification techniques:

The SWRL part is:

professorOf(x, y) -> instructorOf(x, y)

The expected output should contain both ObjectPropertyAssertion( :professorOf :DrBoffin :Bob ) and ObjectPropertyAssertion( :instructorOf :DrBoffin :Bob ). However, the actual output is (showing only object properties)

ObjectPropertyAssertion( :r1 :Bob :Bob )
ObjectPropertyAssertion( :professorOf :DrBoffin :Bob )
ObjectPropertyAssertion( :r2 :DrBoffin :DrBoffin )
ObjectPropertyAssertion( :supervises :DrBoffin :Bob )
ObjectPropertyAssertion( :worksAt :DrBoffin :UF)

Why isn't the expected SWRL result showing up? Any suggestions?

Answer 1

After re-reading your question, I realized that the rule you are trying to represent is

worksAt(x, y), University(y), supervises(x, z), Student(z) → professorOf(x, z)

but that you are trying to represent it, essentially by

(worksAt some University)(x), supervises(x, z), Student(z) → professorOf(x, z)

which is actually a valid SWRL rule, even though it has a complex class expression. (See Can OWL Class Expressions be used in SWRL Rules? for more information. Even though they're valid, the Protégé editor didn't accept that input, though it would display rules correctly if they are already in the ontology.)

Although it can be expressed in SWRL, that will only cover cases where the individuals are named, so the rolification based solution will cover more cases. So, the idea is to create a role rWorksAtSomeUniversity (the rolification of worksAt some University) and a role rStudent (the rolification of Student, and then to assert that

rWorksAtSomeUniversity o supervises o rStudent SubPropertyOf professorOf

Then, to relate professorOf and instructorOf, you can either use a SWRL rule

professorOf(x,y) → instructorOf(x,y)

or a subproperty axiom

professorOf SubPropertyOf instructorOf

As with rolification-based rule, the non-SWRL rule will cover more cases, and does not require that the reasoner have SWRL support.

Here's an ontology that contains these classes and axioms, in the OWL functional syntax. It's not wonderfully human readable, but it's complete; you should be able to download it and test it out with your reasoner.

Prefix(xsd:=<http://www.w3.org/2001/XMLSchema#>)
Prefix(owl:=<http://www.w3.org/2002/07/owl#>)
Prefix(ex:=<http://www.example.com/university#>)
Prefix(xml:=<http://www.w3.org/XML/1998/namespace>)
Prefix(rdf:=<http://www.w3.org/1999/02/22-rdf-syntax-ns#>)
Prefix(rdfs:=<http://www.w3.org/2000/01/rdf-schema#>)

Ontology(<http://www.example.com/university>

Declaration(Class(ex:Professor))
Declaration(Class(ex:Student))
EquivalentClasses(ex:Student ObjectHasSelf(ex:rStudent))
Declaration(Class(ex:University))
Declaration(ObjectProperty(ex:instructorOf))
Declaration(ObjectProperty(ex:professorOf))
SubObjectPropertyOf(ex:professorOf ex:instructorOf)
Declaration(ObjectProperty(ex:rStudent))
Declaration(ObjectProperty(ex:rWorksAtSomeUniversity))
Declaration(ObjectProperty(ex:supervises))
Declaration(ObjectProperty(ex:worksAt))
Declaration(NamedIndividual(ex:Bob))
ClassAssertion(ex:Student ex:Bob)
Declaration(NamedIndividual(ex:DrBoffin))
ClassAssertion(ex:Professor ex:DrBoffin)
ObjectPropertyAssertion(ex:supervises ex:DrBoffin ex:Bob)
ObjectPropertyAssertion(ex:worksAt ex:DrBoffin ex:UF)
Declaration(NamedIndividual(ex:UF))
ClassAssertion(ex:University ex:UF)
EquivalentClasses(ObjectHasSelf(ex:rWorksAtSomeUniversity) ObjectSomeValuesFrom(ex:worksAt ex:University))
SubObjectPropertyOf(ObjectPropertyChain(ex:rWorksAtSomeUniversity ex:supervises ex:rStudent) ex:professorOf)
)

Both Pellet and HermiT 1.3.7 can produce the inferences:

DrBoffin professorOf Bob
DrBoffin instructorOf Bob