Blackout Support for OWL
This page details the Blackout reasoner’s support for OWL axioms.
Page Contents
Overview
The SL reasoning profile supported by Blackout is a superset of QL, EL, and RL profiles. The Blackout inference engine in Stardog employs a query-rewriting approach for inference and consistency-checking. Computing inferences is a separate process from checking consistency. The OWL axioms and expressions supported for inference and consistency checking differ significantly.
In the following sections, we describe in detail the supported axioms and expressions for each task using the OWL functional syntax. See the Mapping to RDF graphs for the RDF representation of these axioms and expressions.
The new Stride reasoner in Stardog differs significantly from Blackout and does not support the SL profile. Please see the Stride documentation for details.
Inference Support
The following OWL axioms are supported for inference under the SL profile with the restrictions described below:
Axioms Supported for Inference:
- SubClassOf
- EquivalentClasses
- SubObjectPropertyOf
- EquivalentObjectProperties
- InverseObjectProperties
- ObjectPropertyDomain
- ObjectPropertyRange
- ReflexiveObjectProperty
- SymmetricObjectProperty
- TransitiveObjectProperty
- SubDataPropertyOf
- EquivalentDataProperties
- DataPropertyDomain
- DataPropertyRange
The below table describes the kind of class expressions supported by the SL profile for SubClassOf
axioms:
Subclass Expressions | Superclass Expressions |
---|---|
a named class | a named class |
an enumeration of individuals (ObjectOneOf ) | intersection of classes (ObjectIntersectionOf ) |
intersection of class expressions (ObjectIntersectionOf ) | negation (ObjectComplementOf ) |
union of class expressions (ObjectUnionOf ) | existential quantification to a class expression (ObjectSomeValuesFrom ) |
existential quantification to a class expression (ObjectSomeValuesFrom ) | universal quantification to a class expression (ObjectAllValuesFrom ) |
existential quantification to a data range (DataSomeValuesFrom ) | existential quantification to an individual (ObjectHasValue ) |
existential quantification to an individual (ObjectHasValue ) | at-most 0/1 cardinality restriction to a class expression (ObjectMaxCardinality 0/1 ) |
existential quantification to a literal (DataHasValue ) | universal quantification to a data range (DataAllValuesFrom ) |
existential quantification to a literal (DataHasValue ) | |
at-most 0/1 cardinality restriction to a data range (DataMaxCardinality 0/1 ) |
Note: This table is a strict superset of how the RL profile is defined. The two additions in the SL profile compared to the RL profile are as follows:
owl:Thing
is allowed as either a subclass or superclass expression.ObjectSomeValuesFrom
is allowed as a superclass expression.
It is also important to note that these restrictions are recursive. This means, for example, ObjectAllValuesFrom
cannot appear inside a subclass expression that is otherwise supported since ObjectAllValuesFrom
is not allowed as a subclass expression. Therefore, the axiom SubClassOf(ObjectSomeValuesFrom(p, ObjectAllValuesFrom(q, C)))
is not supported.
The restrictions for SubClassOf
axioms imply restrictions on the EquivalentClasses
axioms due to the logical equivalence:
This means an EquivalentClasses
axiom is supported only if both SubClassOf
axioms satisfy the conditions from the above table. In other words, all the classes in the equivalence axiom should satisfy the conditions for the subclass and superclass expressions in the above table.
If reasoning.approximate
is set to true, Blackout will split each EquivalentClasses
axiom into two and will use the subclass axiom(s) that satisfy the above conditions and ignore those that do not.
The restrictions on class expressions affect other axioms where class expressions may appear: ObjectPropertyDomain
, ObjectPropertyRange
, and DataPropertyDomain
. The class expressions appearing in these axioms should satisfy the superclass restrictions.
The SL profile supports both ObjectProperty
and InverseObjectProperty
expressions in axioms with property expressions. There is only one restriction:
- The built-in
owl:topObjectProperty
cannot be used in any axiom except in the super-property position of aSubObjectPropertyOf
axiom.
Note that, by definition, the ObjectPropertyChain
can only be used in the sub-property position of a SubObjectPropertyOf
axiom. Furthermore, property axioms should satisfy the Global Restrictions on Property Hierarchies defined in the OWL specification.
SameAs Support
Blackout can infer owl:sameAs
triples if Same As reasoning is enabled, using these axioms when configured (reasoning.sameas=FULL
):
- FunctionalObjectProperty
- InverseFunctionalObjectProperty
- HasKey
Consistency Support
The Blackout reasoner uses these axioms for consistency checking:
- DisjointClasses
- DisjointObjectProperties
- DisjointDataProperties
- AsymmetricObjectProperty
- IrreflexiveObjectProperty
- FunctionalDataProperty
- DataPropertyRange
Class expressions in DisjointClasses
must satisfy subclass restrictions due to:
ObjectMaxCardinality
and DataMaxCardinality
as superclasses in SubClassOf
axioms trigger inconsistency if:
ObjectMaxCardinality
is 0 with an IRI class.DataMaxCardinality
is 0 or 1.
Higher cardinality restrictions are ignored in consistency checking.