MobiBench: OWL2 RL optimizations

This page details a number of entailments that enable the identification of equivalent OWL2 RL rule subsets. In particular, these entailments indicate that, aside from two selections, each rule subset selection retains full conformance with OWL2 RL (i.e., they do not result in loss of expressivity). For "Equivalence with instance-based rules", we show that, although certain schema inferences will be missing, these do not result in missing instance inferences. Further, for "Removal of inefficient rules", we show that only a particular consistency-checking case will be no longer supported.

MobiBench allows automatically selecting such rule subsets.

Contact: William Van Woensel

• Equivalent OWL2 RL subset
  • Entailments between OWL2 RL rules
  • Extra supporting axiomatic triples
  • New generalized OWL2 RL rules
  • Equivalence with instance-based rules
• Purpose- and reference-based subsets
• Removal of inefficient rules

This section lists logical entailments between OWL2 RL rules.

Entailed by #cax-sco

These rules are entailed by the #cax-sco rule, each time combined with a second inference rule.

Combined with #scm-uni

1) #cax-sco and #scm-uni entail the rule #cls-uni:

Applying #scm-uni on two premises from #cls-uni returns inference (1). Then, #cax-sco is applied on the remaining premise, together with (1). This yields the inference in (2), which equals the #cls-uni consequent.

Combined with #scm-int

1) #cax-sco and #scm-int entail the rule #cls-int2:

Applying #scm-int on two premises from #cls-int2 returns inference (1). Then, #cax-sco is applied on the remaining premise, together with (1). This yields the inference in (2), which equals the #cls-int2 consequent.

Combined with #scm-eqc1

1) #cax-sco and #scm-eqc1 entail the rule #cax-eqc1:

Applying #scm-eqc1 on the first premise from #cax-eqc1 returns inference (1). Then, #cax-sco is applied on the remaining premise, together with (1). This yields the inference in (2), which equals the #cax-eqc1 consequent.

2) very similarly, #cax-sco and #scm-eqc1 entail the rule #cax-eqc2:

Applying #scm-eqc1 on one premise from #cax-eqc2 returns inference (1). Then, #cax-sco is applied on the remaining premise, together with (1). This yields the inference in (2), which equals the #cax-eqc2 consequent.

Entailed by #prp-spo1

These rules are entailed by the #prp-spo1 rule, each time combined with rules indicating equivalence between owl:equivalent[Class|Property] and rdfs:sub[Class|Property]Of.

Combined with #scm-eqp1

1) #prp-spo1 and #scm-eqp1 entail the rule #prp-eqp1:

Applying #scm-eqp1 on the first premise of #prp-eqp1 returns inference (1). Then, #prp-spo1 is applied on the remaining premise, together with (1). This yields the premise in (2), which equals the #prp-eqp1 consequent.

2) very similarly, #prp-spo1 and #scm-eqp1 entail the rule #prp-eqp2:

Applying #scm-eqp1 on the first premise of #prp-eqp2 returns inference (1). Then, #prp-spo1 is applied on the remaining premise, together with (1). This yields the premise in (2), which equals the #prp-eqp2 consequent.

Entailed by #eq-rep-o

1) #eq-rep-o entails #eq-trans:

When executing the #eq-rep-o rule on relevant data, the ?p variable will be instantiated with owl:sameAs, thus covering each possible inference of #eq-trans.

This section lists possibilities to introduce extra axioms, allowing us to leave out certain rules.

Entailed by #prp-symp

These rules are entailed by #prp-symp, each time combined with an extra axiom and, potentially, a second rule.

1) #prp-symp & extra axiom entail #eq-sym:

Typing the sameAs property as a SymmetricProperty and applying #prp-symp on the #eq-sym premise yields inference (1), which equals the #eq-sym consequent.

2) #prp-symp, #prp-inv1 & extra axiom entail #prp-inv2:

Typing the inverseOf property as a SymmetricProperty and applying #prp-symp on the first premise of #prp-inv2 returns inference (1). Then, #prp-inv1 is applied on the remaining premise, together with (1). This yields the premise in (2), which equals the #prp-inv2 consequent.

Entailed by #prp-trp

These rules are entailed by #prp-trp, each time combined with an extra axiom.

1) #prp-trp & extra axiom entail #scm-sco:

Typing the subClassOf property as a TransitiveProperty and applying #prp-trp on the two premises of scm-sco returns inference (1), which equals the #scm-sco consequent.

2) very similarly, #prp-trp & extra axiom entail #scm-spo:

Typing the subPropertyOf property as a TransitiveProperty and applying #prp-trp on the two premises of scm-spo returns inference (1), which equals the #scm-spo consequent.

This section lists possibilities for introducing new generalized rules & supporting axioms, which allows us to leave out certain specialized rules.

New #prp-sl rule

Rules #eq-rep-p and #prp-spo1 are structurally very similar:

Both may be generalized into a single new rule, with accompanying axioms:

New #scm-vr rule

Rules #scm-hv and #scm-svf2 are structurally very similar:

Both may be generalized into a single new rule, with accompanying axioms:

New #scm-mvr rule

Rules #scm-avf1 and #scm-svf1 are structurally very similar:

Both may be generalized into a single new rule, with accompanying axioms:

New #eq-diff rule

Rules #eq-diff2 and #eq-diff3 are structurally very similar:

Both may be generalized into a single new rule, with accompanying axioms:

New #prp-npa rule

Rules #prp-npa1 and #prp-npa2 are structurally very similar:

Both may be generalized into a single new rule, with accompanying axioms:

New #cls-dsj rule

Rules #cls-com and #cax-dw are structurally very similar:

Both may be generalized into a single new rule, with accompanying axioms:

This section lists entailments showing that certain inferred schema elements will not lead to new instances being inferred. As such, they can be considered redundant at the instance level. However, we note that these schema elements could be considered valuable additions to the ontology itself, regardless of their capability of inferring new instances.

1) instance inferences from #scm-dom1 are covered by #prp-dom & #cax-sco:

Rule #scm-dom1 generates a new schema element:

Based on the new element T(?p, domain, ?c2), rule #prp-dom can then generate new instance inferences:

Below, we show that these instance inferences are already covered by rules #prp-dom (1) and #cax-sco (2):

$$T(?s, ?p, ?o), T(?p, domain, ?c_{1}) \rightarrow T(?s, type, ?c_{1}) \hspace{10px} (1)\\ T(?s, type, ?c_{1}), T(?c_{1}, subClassOf, ?c_{2}) \rightarrow T(?s, type, ?c_{2}) \hspace{10px} (2)$$

2) very similarly, instance inferences from #scm-rng1 are covered by #prp-rng & #cax-sco:

Rule #scm-rng1 generates a new schema element:

Based on the new element T(?p, range, ?c2), rule #prp-rng can then generate new instance inferences :

Below, we show that these instance inferences are already covered by rules #prp-rng (1) and #cax-sco (2):

$$T(?s, ?p, ?o), T(?p, range, ?c_{1}) \rightarrow T(?o, type, ?c_{1}) \hspace{10px} (1)\\ T(?o, type, ?c_{1}), T(?c_{1}, subClassOf, ?c_{2}) \rightarrow T(?o, type, ?c_{2}) \hspace{10px} (2)$$

3) instance inferences from scm-dom2 are covered by #prp-dom & prp-spo1:

Rule #scm-dom2 generates a new schema element:

Based on the new element T(?p1, domain, ?c), rule #prp-dom can then generate new instance inferences:

Below, we show that these instance inferences are already covered by rules #prp-spo1 (1) and #prp-dom (2):

$$T(?s, ?p_{1}, ?o), T(?p_{1}, subPropertyOf, ?p_{2}) \rightarrow T(?s, ?p_{2}, ?o) \hspace{10px} (1) \\ T(?s, ?p_{2}, ?o), T(?p_{2}, domain, ?c) \rightarrow T(?s, type, ?c) \hspace{10px} (2)$$

4) very similarly, instance inferences from scm-rng2 are covered by #prp-rng & prp-spo1:

Rule #scm-rng2 generates a new schema element:

Based on the new element T(?p1, range, ?c), rule #prp-rng can then generate new instance inferences:

Below, we show that these instance inferences are already covered by rules #prp-spo1 (1) and #prp-rng (2):

$$T(?s, ?p_{1}, ?o), T(?p_{1}, subPropertyOf, ?p_{2}) \rightarrow T(?s, ?p_{2}, ?o) \hspace{10px} (1) \\ T(?s, ?p_{2}, ?o), T(?p_{2}, range, ?c) \rightarrow T(?o, type, ?c) \hspace{10px} (2)$$

Since ABox (instance) statements are the only statements likely to be added at runtime, an option is to only perform TBox (schema) reasoning once at startup, or whenever the ontology changes; and ABox reasoning each time new instances are added. Further, we note that in case data is automatically generated by the system, it has a lower likelihood of being in consistent, thus removing the need for continuous consistency checking.

Consequently, we divided our OWL2 RL ruleset into 2 major subsets; 1) inference ruleset, comprising inference rules (53 rules), and 2) consistency-checking ruleset, containing consistency checking rules (18 rules). The inference ruleset is further subdivided into 1.1) instance ruleset, consisting of rules referring both instance and schema elements (32 rules); and 1.2) schema ruleset, comprising rules only referencing schema elements (23 rules). Since the consistency-checking ruleset only contains rules referring to both instance and schema elements, it cannot be further subdivided.

To ensure OWL2 RL-conformant inferences, the inference-instance rule subset (1.1) needs to be applied to an ontology in which schema-based inferences are already materialized. For this purpose, the inference-schema (1.2) subset is applied on the initial ontology. (For proof that this sequential application of rule subsets is equivalent to applying the entire ruleset, we refer to [1].) For instance, this may be done at design-time or install-time, and on ontology updates.The utility of separating these subsets clearly depends on the frequency of ontology updates, since each update requires re-materializing the ontology (depending on the concrete scenario, ontology updates may be infrequent; at least compared to instance data). Similarly, the concistency-checking ruleset needs to be applied on data where all inferences have been materialized, by applying the inference rule subset.

Further, certain rules, not referenced by the schema or instance dataset, may be left out as well. For this purpose, we implemented a domain-based ruleset selection algorithm, which is available from our web service (see Tai et al. [2] for details on this algorithm). Similar to separating instance and schema rulesets, its applicability depends on the frequency (and, also the significance) of ontology updates; since this requires re-calculating the ruleset.

Our web service allows creating custom OWL2 RL rule subsets by automatically applying (individually or together) any of the presented ruleset selections.

The #eq-ref rule has the potential to greatly bloat the dataset: $$T(?s,?p,?o) \rightarrow T(?s,sameAs,?s), T(?p,sameAs,?p),T(?o,sameAs,?o)$$

For each unique resource, this rule creates a new statement indicating the resource's equivalence to itself. Consequently, 3 new triples are generated for each triple with unique resources, resulting in a worst-case 4x increase in dataset size (!). One could argue that there is limited practical use in materializing these self-equivalency statements: especially seeing how leaving them out will not influence other inferences, although it could influence consistency-checking in one particular case.

To see why leaving out these self-equivalency statements does not influence other inferences, we need to look at rules that reference owl:sameAs statements.

Inference rules

Rule #eq-sym

Instantiating this rule with a self-equivalency statement T(X, sameAs, X) yields the following inference:

The same statement is again inferred, meaning no additional inferences are made.

Rule #eq-trans

All possible instantiations of this rule with a self-equivalency statement T(X, sameAs, X) results in the following inferences:

In all cases, one of the instantiated premises is simply inferred again, meaning no additional inferences are made.

Rule #eq-rep-s

Instantiating this rule with a self-equivalency statement T(X, sameAs, X) yields the following inference:

This rule simply infers the second premise again, meaning no additional inferences are made.

Rule #eq-rep-p

Instantiating this rule with a self-equivalency statement T(X, sameAs, X) yields the following inference:

This rule simply infers the second premise again, meaning no additional inferences are made.

Rule #eq-rep-o

Instantiating this rule with a self-equivalency statement T(X, sameAs, X) yields the following inference:

This rule simply infers the second premise again, meaning no additional inferences are made.

Consistency-checking rules

On the other hand, leaving out the #eq-ref rule could have an impact on consistency-checking performed by the #eq-diff1 rule:

In case of reciprocal statements such as T(X, differentFrom, X), this rule will only be triggered in case X's self-equivalency statement (i.e., T(X, sameAs, X)) is also present. Therefore, in this particular case, this consistency-checking rule will no longer fire.

Regarding the remaining two consistency-checking rules that reference sameAs statements (see below): these cannot fire for self-equivalency statements due to the condition ?y1 != ?y2. We note that this condition always needs to be present, else the two clauses T(?list, hasMember, ?y1) and T(?list, hasMember, ?y2) will fire for a single hasMember triple.

References