Ontoprise OWLRL in ObjectLogic

From ONTORULE Show Case

Motivation

Description

The OWL RL profile defines a syntactic subset of OWL 2 that is aimed at applications requiring scalable reasoning without sacrificing too much expressive power. There are a number of experimental implementations available Jena, Ivan Herman, as well as first industrial implementations Oracle Database 11g OWL Reasoner, OWLIM. The ontoprise inferencing component, realized within ONTORULE as a tight coupling approach for OWL ontologies and logic programming rules, has been built on top of the OntoBroker ObjectLogic reasoner. The OWL-specific syntactical elements have been mapped to existing ObjectLogic constructs or have been added as new predicates. The axioms defining the RL profile have been added as ObjectLogic rules or constraints.

Syntax

For the syntax of OWL-in-ObjectLogic, every OWL construct which has an equivalent construct in ObjectLogic is mapped directly, in particular subClassOf is mapped to :: and subPropertyOf is mapped to <<. All OWL constructs which do not have an equivalent in ObjectLogic are mapped to special predicates, for example owl:sameAs is mapped to ObjectLogic _SameIndividual, owl:allValuesFrom is mapped to _AllValuesFrom. Our implementation differs from the specification in the following details:

1. We make no distinction between ObjectProperty and DataProperty constructs.
2. We do not support restrictions using n-ary data range.
3. Some predicates are rewritten internally as predicates with additional facts, needed by the axiomatization.

As an example, the OWL construct owl:oneOf is represented by the ObjectLogic predicate _OneOf and has the internal representation $OneOf. The first position in the internal predicate $OneOf(?, ?c,?y) is placeholder for an internal unique id, ?c is the name of the complex class and ?y represents a list variable.

Semantics

The standard ruleset defining the OWL RL profile is given by about 70 named entailment rules, which can be roughly grouped into rules defining the owl:sameAs equality (eq-ref, eq-sym, eq-trans,…), rules describing the semantics of complex classes (cls-uni,cls-int…) rules for algebraic, inverse and functional properties (prp-fp …) and rules describing property chains and keys (prp-spo-1, prp-spo-2). The OWL RL axioms have been implemented as ObjectLogic rules. The ontoprise implementation has some specifics. The implementation uses constraints for a number of OWL constructs, in particular for disjoint classes, keys, cardinality restrictions, functional and inverse functional properties and for the equality axiom @{'eq-diff1'}. We also make the closed world assumption. In core ObjectLogic we make the unique name assumption and state a constraint violation if two individuals having different identifiers are declared as same: !- _SameIndividual(?x,?y) AND NOT ?x=?y. For OWL-in-ObjectLogic we developed additionally a concept named ground equality. _SameIndividual(?x,?y) is not inferred. Internally we create equivalence classes for same individuals. In a third variant shown below the owl:sameAs construct is fully axiomatized.

Axioms

In the following we show some examples. For the complete description check D3.3 Chapter 3.

Example: owl:sameAs equality fully axiomatized

Axiom eq-diff1 has been formulated as a constraint. If two individuals have been declared as same and different, we have a constraint violation. The axioms eq-diff2 and eq-diff3 define the semantics for the owl:AllDifferent construct, in ObjectLogic denoted by _DifferentIndividuals1. The auxiliary axiom reduce-diff reduces _DifferentIndividuals1, the construct for a list with mutually different members, to _DifferentIndividuals, the predicate for a list with 2 different members.

// Reflexivity axiom
@{'eq-ref'} _SameIndividual(?s,?s) AND _SameIndividual(?p,?p) AND _SameIndividual(?o,?o):-?s[?p ->?o].
// Symmetry axiom
@{'eq-sym'} _SameIndividual(?y,?x) :- _SameIndividual(?x,?y).
// Transitivity axiom
@{'eq-trans'} _SameIndividual(?x,?z) :- _SameIndividual(?x,?y) AND _SameIndividual(?y,?z).
// Equality of subjects
@{'eq-rep-s'} ?s1[?p ->?o] :- _SameIndividual(?s,?s1) AND ?s[?p ->?o].
// Equality of properties
@{'eq-rep-p'} ?s[?p1 ->?o]:- _SameIndividual(?p,?p1) AND ?s[?p ->?o].
@{'eq-diff1'} !- _SameIndividual(?x,?y) AND _DifferentIndividuals(?x,?y).
@{'eq-diff2'} _DifferentIndividuals(?A, ?B) :- 
_DifferentIndividuals1(?X) AND ?X[_member->?A] AND ?X[_member->?B] AND NOT _unify(?A, ?B).
@{'eq-diff3'} _SameIndividual(?A, ?B) :- 
_SameIndividual1(?X) AND ?X[_member->?A] AND ?X[_member->?B].
@{'reduce-diff'} _DifferentIndividuals(?i,?j) :- 
_DifferentIndividuals1(?x) AND ?x[_member->?i] AND ?x[_member->?j] AND NOT _SameIndividual(?i,?j).

Example: owl:intersectionOf class construct

Axiom cls-int1 has been split in 9 axioms for lists up to n=9 members (n is an arbitrary number, chosen for performance reasons). For longer lists, recursion is used. Axiom scm-int has been implemented in a similar way.

@{'cls-int1-2'} ?y:?c :- $IntersectionOf2(?,?c,?c1,?c2) AND ?y:?c1 AND ?y:?c2.
@{'cls-int1-3'} ?y:?c :- $IntersectionOf3(?,?c,?c1,?c2,?c3) AND ?y:?c1 AND ?y:?c2 AND ?y:?c3.
...
@{'cls-int1-8'}
@{'scm-int-2'} 
?c::?c1 AND ?c::?c2 :- $IntersectionOf2(?,?c,?c1,?c2).
@{'scm-int-3'} 
?c::?c1 AND ?c::?c2 AND ?c::?c3 :- $IntersectionOf3(?,?c,?c1,?c2,?c3).
@{'scm-int-4'} 
?c::?c1 AND ?c::?c2 AND ?c::?c3 AND ?c::?c4 :- $IntersectionOf4(?,?c,?c1,?c2,?c3,?c4).
...
@{'scm-int-8'}

Example: owl:hasValue class construct The owl:hasValue class construct groups all the individuals ?u from a domain ?x having the same value ?y for a given property ?p.

@{'cls-hv1'} ?u[?p -> ?y] :- $HasValue(?,?x,?p,?y) AND ?u:?x.
@{'cls-hv2'} ?u:?x :- $HasValue(?,?x,?p,?y) AND ?u[?p -> ?y].
@{'scm-hv'} ?c1::?c2 :- $HasValue(?,?c1,?p1,?i) AND $HasValue(?,?c2,?p2,?i) AND ?p1<<?p2.

Constraints

An ObjectLogic constraint is a special type of rule without a rule head that when queried returns all individuals violating the constraint.

Example: Disjoint Classes

We axiomatize the semantics of disjoint classes using the following constraint, which states a constraint violation if an individual ?x is detected, which belongs to two disjoint classes ?c1 and ?c2.

!- _DisjointClasses(?c1,?c2) AND ?x:?c1 AND ?x:?c2 AND ?EX = "Detected individual in the intersection of two disjoint classes."

Tests

We performed a series of syntactical and syntax translation tests, followed by semantical tests for the axiomatization part.

The (positive and negative) entailment tests cover the OWL2 RL Test Cases.

Example: Entailment test for the combination owl:intersectionOf and owl:hasValue

In the test ontology below, a is in the result ontology (positive entailment) and d is not, since z is not in the complex class (negative entailment).

//Schema
_IntersectionOf([_HasValue(p,v),_HasValue(q,w)])::C.

// Instances
a[p->v].
a[q->w].
b[p->v].
c[q->w].
d[p->z].
d[q->z].

//Axioms @{'cls-hv1'}, @{'cls-hv2'}, @{'cls-int1-2'}, ...

// Query
?- ?i:C.

//Expected results
a