Validating RDF with OWL Integrity Constraints

Authors:
Héctor Pérez-Urbina, Clark & Parsia, LLC
Evren Sirin, Clark & Parsia, LLC
Kendall Clark, Clark & Parsia, LLC

Abstract

This document proposes a method for validating Semantic Web and Linked Data by providing an alternative, integrity constraint (IC) semantics for OWL. A model-theoretic semantics based on the Closed World Assumption and a weak variant of the Unique Name Assumption is given for OWL axioms that are thereby interpreted as ICs. The document includes a structural specification in order to augment an ontology with a set of OWL ICs and a brief description of possible implementation approaches.

Table of Contents

1. Introduction

This document proposes a method of constraining and validating Semantic Web and Linked Data (i.e., RDF) instance data using Integrity Constraints (ICs) modeled as OWL axioms. The proposal enables an OWL ontology to be interpreted as a set of ICs; i.e., checks that must be satisfied by the information explicitly present or information that may be inferred. We define a model-theoretic semantics for OWL ICs based on the Closed World Assumption and a weak variant of the Unique Name Assumption and briefly describe feasible implementation strategies.

In some use cases and for some requirements, OWL users intend OWL axioms to be interpreted as ICs. However, the direct semantics of OWL [OWL 2 Direct Semantics] does not interpret OWL axioms in this way; thus, the consequences that one can draw from such ontologies differ from the ones that some users intuitively expect and require. In other words, some users want to use OWL as a validation or constraint language for RDF instance data, but that is not possible using OWL software that correctly implements the existing semantics of OWL. This document addresses that situation by providing a different semantics—compatible with the existing semantics—for OWL axioms which may be used, together with appropriate software, to validate RDF instance data.

To see the nature of the problem, consider an OWL ontology that describes terms and concepts regarding the product inventory of a supermarket. The ontology includes the classes Product and Provider, the object property hasProvider, and the data property hasID. Suppose we want to impose the following ICs on the data:

  1. Each product must have an ID
  2. Only products can have IDs
  3. Products must not have more than one provider

These constraints could be interpreted in the following way:

  1. Whenever an instance producti of Product is added to the ontology, a check should be performed to verify whether the ID of producti has been specified; if not, the update should be rejected.
  2. Whenever an instance <producti, IDi> of hasID is added to the ontology, a check should be performed to verify whether producti is an instance of Product; if not, the update should be rejected.
  3. Whenever an instance <producti, provideri> of hasProvider is added to the ontology, a check should be performed to verify whether another provider providerj has been specified for producti; if so, the update should be rejected.

These constraints can be concisely and unambiguously represented as OWL axioms:

  1. Class: Product 
    hasID some literal
  2. DataProperty: hasID 
    Domain: Product
  3. ObjectProperty: hasProvider 
    Characteristics: Functional

However, these axioms will not be interpreted as checks by software which implements the standard OWL semantics. In fact, according to the standard OWL semantics, we have that:

  1. Adding a product without an ID to the ontology does not raise an error, but leads to the inference that the product in question has an unknown ID.
  2. Adding a tuple <producti, IDi> to the ontology without producti being an instance of Product does not raise an error, but leads to the inference that producti is an instance of Product.
  3. Adding a tuple <producti, provideri> having specified a previous provider providerj for producti does not raise an error, but leads to the inference that provideri and providerj denote the same individual.

In some cases, users want these inferences; but in others, users want integrity constraint violations to be detected, reported, repaired, etc.

OWL adopts the Open World Assumption (OWA) and does not adopt the Unique Name Assumption (UNA). These design choices make it very difficult to treat these axioms as ICs. On the one hand, due to OWA, a statement must not be inferred to be false on the basis of failures to prove it; therefore, the fact that a piece of information has not been specified (e.g., a product's ID) does not mean that such information does not exist. On the other hand, the absence of UNA allows two different constants to refer to the same individual (e.g., provideri and providerj).

The standard interpretation of OWL axioms that are intended to be interpreted as ICs is inappropriate for some use cases and applications; therefore, it is useful to define an alternate semantics for OWL based on IC. An IC semantics together with associated software will increase the number of satisfied users of OWL because OWL and the software will then behave as those users intuitively expect and require.

As formally defined in Section 2, our approach allows for a standard OWL ontology O to import a set of IC ontologies—OWL ontologies that are to be interpreted as ICs. Note that the IC semantics for OWL defined in this document is a strict extension of the standard OWL semantics: in case O imports no IC ontology, then O should be interpreted as a standard OWL ontology.

2. Structural Specification

An OWL ontology that is to be interpreted as a set of ICs is called an IC ontology. We slightly extend the structural specification of OWL in order to allow ontologies to import a set of IC ontologies. We do so by introducing a new annotation property which is defined analogously to owl:imports—the annotation property that is used to import standard ontologies defined by OWL 2 [OWL 2 Specification].

We use an annotation property that resembles owl:imports with a different namespace: http://www.w3.org/Submission/owlic/. In the following, we denote this annotation property as ic:imports for brevity.

An example usage of this annotation property is given in the following:

Namespace(ic = <http://www.w3.org/Submission/owlic/>)
Ontology(<http://www.example.com/instanceOntology>
	Import(<http://www.example.com/schemaOntology>)
	Annotation(ic:imports <http://www.example.com/constraintsOntology>)
	...
)

where instanceOntology imports the standard axioms of schemaOntology and imports constraintsOntology as an IC ontology. This import approach to relating ICs to other OWL ontologies gives enough flexibility to users without too much maintenance cost and negligible impact on existing tools. See Implementation Remarks for a more detailed discussion of this design choice.

An OWL ontology can import a set of IC ontologies via ic:imports. An IC ontology can import a set of IC ontologies via ic:imports as well. And, of course, an IC ontology can import a set of standard ontologies via owl:imports as usual.

The import closure of an IC ontology is defined in the same vein as the import closure for standard OWL ontologies. The IC import closure of a standard or IC ontology O is a set containing all the IC ontologies that O imports via the ic:imports annotation property. The IC closure of a standard or IC ontology O is the smallest set that contains all the axioms from each ontology O' in the IC import closure of O.

3. OWL IC Semantics

We refer to the definitions of datatype map, vocabulary, and OWL interpretation and model in OWL 2 [OWL 2 Direct Semantics].

3.1 IC-Interpretations

Let D = (NDT, NLS, NFS, ·DT, ·LS, ·FS) be a datatype map and let V = (VC, VOP, VDP, VI, VDT, VLT, VFA) be a vocabulary over D. An IC-interpretation Γ = (ΔI, ΔD, I, U, ·C, ·OP, ·DP, ·I, ·DT, ·LT, ·FA) for D and V is an 11-tuple with the following structure:

The extensions of · C, · OP, and · DT to class expressions, object property expressions, and data ranges respectively, are defined analogously to OWL 2 [OWL 2 Direct Semantics]. For example, we extend · C to the class expression ObjectIntersectionOf(CE1 ... CEn) as (CE1)C ∩ ... ∩ (CEn)C. However, we extend · C to ObjectComplementOf(CE) as {xI | x ∈ VI} \ (CE)C—that is, the complement of a class expression is defined with respect to the set of named individuals as opposed to the object domain. The complete extensions for · C, · OP, and · DT can be found in the Appendix.

3.2 Axiom Satisfaction

Satisfaction of an IC-interpretation Γ with respect to a given axiom is defined analogously to satisfaction of standard intepretations defined in OWL 2 [OWL 2 Direct Semantics]. For example, Γ satisfies the axiom SubClassOf(CE1 CE2) if (CE1)C(CE2)C. The complete definitions for axiom satisfaction can be found in the Appendix.

3.3 Axiom IC-Satisfaction

Let D = (NDT, NLS, NFS, ·DT, ·LS, ·FS) be a datatype map and let V = (VC, VOP, VDP, VI, VDT, VLT, VFA) be a vocabulary over D.

3.4 Inference Problem

We are mainly interested in the following inference problem:

Ontology Validation. Let O be an OWL ontology. We say that O is Valid iff for all axioms α in the IC closure of O, it holds that O IC-satisfies α.

4. Implementation Remarks

4.1 Implementing IC Syntax

As discussed in Section 2, we use standard OWL syntax for ICs; store ICs in a separate document; and define a new annotation property analogous to owl:imports, that will associate a standard OWL ontology with a set of ICs defined for that ontology.

The motivation for this design choice is to minimize the effects of ICs on existing tools. From the perspective of creation and maintenance, users can continue using existing ontology authoring toolsets. For example, one can use an OWL editor to create ICs and store them in a document. The ontology for which the constraints are written can be augmented with the IC import annotation easily, since this is a standard OWL annotation. With an OWL editor that allows users to open and edit multiple ontologies at the same time, the regular ontology and the IC ontology can be edited together. Several OWL editors provide the feature to move axioms between ontologies; hence, one can easily change the interpretation of an axiom just by moving it from the regular ontology to the IC ontology.

The only issue in using an existing OWL editor is as follows: when a user opens a regular ontology that links to an IC ontology, the editor will not open the IC ontology automatically. The user needs to look at the ontology annotation and open the IC ontology manually. However, this is not a serious issue since it is a relatively simple extension for editors to recognize this annotation. It is safe to assume that such extensions will be available, especially if ICs start to be widely used.

Our approach has no impact on OWL existing reasoners that do not support ICs: since the annotation property has no semantic effect, they would not process that annotation. Therefore, there is no additional work that needs to be done to hide the ICs in order to avoid unintended inferences that would occur if they are inadvertently interpreted as regular OWL axioms.

Note that our approach does not require an IC ontology to be identified as such. However, in case an ontology is to be exclusively interpreted as a set of ICs, one might use an ontology annotation to make this fact explicit. As usual, such annotations are for informational purposes only and have no effect on the semantics.

4.2 Implementing IC Semantics

The IC semantics described in this document is strongly related to the semantics presented in a paper [TSBM10] giving a formal integrity constraint semantics for the description logic SROIQ. Based on the correspondence between SROIQ and OWL 2 semantics [OWL 2 Direct Semantics], the semantics we present here has been adapted to OWL 2 and extended to support datatypes.

As discussed in the paper, there is a close relationship between IC semantics and queries that have negation as failure (NAF) operator. This is interesting from a practical point of view because a validator for OWL IC can be implemented in a straightforward way: each axiom in an IC ontology defined with respect to an OWL ontology O can be effectively transformed into a SPARQL query that can be later answered over O using the SPARQL entailment regime that corresponds to O.

As a simple example of the translation, consider the IC presented in Example 6 above:

Class: Supervisor 
   SubClassOf: supervises some Employee

The translation of this IC to SPARQL would yield the following SPARQL query:

ASK WHERE { 
   ?x rdf:type :Supervisor . 
   OPTIONAL {
      ?x :supervises ?y . 
      ?y rdf:type :Employee . 
   }
   FILTER ( !bound( ?y ) )
}

If the execution of the query over an ontology O returns true, we can conclude that the IC has been violated by O; and, therefore, that O is not IC-valid with respect to this constraint. Note that the query uses the OPTIONAL/FILTER/!BOUND pattern to encode NAF. However, it is likely that SPARQL 1.1 [SPARQL 1.1] will make NAF more clearly visible syntatically, perhaps via NOT EXISTS as in current drafts.

It has been shown that SPARQL [SPARQL] has the same expressive power as nonrecursive datalog programs with NAF [AG08]. Therefore, it is possible to translate OWL ICs to a set of rules that will be evaluated over an ontology O. Such rules can be written using RIF Framework for Logic Dialects [RIF-FLD] with the Naf operator:

Forall ?x ?y (
    invalid() :- And (
        ?x[rdf:type -> :Supervisor]
        Naf And (
            ?x[:supervises -> ?y]
            ?y[rdf:type -> :Employee] )))

This rule uses the Naf operator for encoding NAF and defines an arbitrary RIF predicate invalid to detect the condition that an ontology O is invalid with respect to ICs. Implementations would be free to choose a different name for the predicate.

Details of the translation are out of the scope here; interested readers are referred to the formal semantics paper mentioned previously [TSBM10]. Translation-based IC validation is one of many possibilities to implement IC validation and has been mentioned here as an example. An IC validator conforming to the IC semantics described here can also be implemented with different approaches.

Acknowledgements

We wish to thank the following people for their assistance: Pavel Klinov, Michael Smith, Michael Grove, Jiao Tao, and Peter Patel-Schneider. We thank members of the OWLED community, including the anonymous reviewers, who gave us very early feedback on using OWL as integrity constraints, including, most helpfully, use cases and requirements. We also acknowledge the support of NIST SBIR funding under the auspices of which this document was prepared.

References

[OWL 2 Direct Semantics]
OWL 2 Web Ontology Language: Direct Semantics. Boris Motik, Peter F. Patel-Schneider, Bernardo Cuenca Grau, eds. W3C Recommendation, 27 October 2009, http://www.w3.org/TR/2009/REC-owl2-direct-semantics-20091027/. Latest version available at http://www.w3.org/TR/owl2-direct-semantics/.
[OWL 2 Specification]
OWL 2 Web Ontology Language: Structural Specification and Functional-Style Syntax. Boris Motik, Peter F. Patel-Schneider, Bijan Parsia, eds. W3C Recommendation, 27 October 2009, http://www.w3.org/TR/2009/REC-owl2-syntax-20091027/. Latest version available at http://www.w3.org/TR/owl2-syntax/.
[SPARQL]
SPARQL Query Language for RDF. Eric Prud'hommeaux and Andy Seaborne, eds. W3C Recommendation, 15 January 2008, http://www.w3.org/TR/2008/REC-rdf-sparql-query-20080115/. Latest version available as http://www.w3.org/TR/rdf-sparql-query/.
[SPARQL-1.1]
SPARQL Query Language 1.1. Steve Harris and Andy Seaborne, eds. W3C Working Draft, 26 January 2010, http://www.w3.org/TR/2010/WD-sparql11-query-20100126/. Latest version available as http://www.w3.org/TR/sparql11-query/.
[TSBM10]
Integrity Constraints in OWL. Jiao Tao, Evren Sirin, Jie Bao, Deborah L. McGuinness. In Proc. of the 24th Conference on Artificial Intelligence (AAAI 2010). Atlanta, USA. 2010.
[AG08]
The Expressive Power of SPARQL. Renzo Angles, Claudio Gutierrez. In Proc. of the 7th International Semantic Web Conference (ISWC 2008). Karlsruhe, Germany. 2008.

Appendix A

A.1 Extensions of Interpretation Functions

A.1.1 Class Expressions

The class interpretation function ·C is extended to class expressions as shown in Table 1. For S a set, #S denotes the number of elements in S.

Table 1. Interpreting Class Expressions
Class Expression Interpretation ·C
ObjectIntersectionOf(CE1 ... CEn ) (CE1)C ∩ ... ∩ (CEn)C
ObjectUnionOf(CE1 ... CEn) (CE1)C ∪ ... ∪ (CEn)C
ObjectComplementOf(CE) { xI| x ∈ VI } \ (CE)C
ObjectOneOf(a1 ... an) { (a1)I, ..., (an)I }
ObjectSomeValuesFrom(OPE CE) { x | ∃ y: (x, y) ∈ (OPE)OP and y(CE)C }
ObjectAllValuesFrom(OPE CE) { x | ∀ y: (x, y) ∈ (OPE)OP implies y(CE)C }
ObjectHasValue(OPE a) { x | (x, (a)I) ∈ (OPE)OP }
ObjectHasSelf(OPE) { x | (x, x) ∈ (OPE)OP }
ObjectMinCardinality(n OPE) { x | #{ y | (x, y) ∈ (OPE)OP } ≥ n }
ObjectMaxCardinality(n OPE) { x | #{ y | (x, y) ∈ (OPE)OP } ≤ n }
ObjectExactCardinality(n OPE) { x | #{ y | (x, y) ∈ (OPE)OP } = n }
ObjectMinCardinality(n OPE CE) { x | #{ y | (x, y) ∈ (OPE)OP and y(CE)C } ≥ n }
ObjectMaxCardinality(n OPE CE) { x | #{ y | (x, y) ∈ (OPE)OP and y(CE)C } ≤ n }
ObjectExactCardinality(n OPE CE) { x | #{ y | (x, y) ∈ (OPE)OP and y(CE)C } = n }
DataSomeValuesFrom(DPE1 ... DPEn DR) { x | ∃ y1, ..., yn: (x, yk) ∈ (DPEk)DP for each 1 ≤ kn and (y1, ..., yn) ∈ (DR)DT }
DataAllValuesFrom(DPE1 ... DPEn DR) { x | ∀ y1, ..., yn: (x, yk) ∈ (DPEk)DP for each 1 ≤ kn imply (y1, ..., yn) ∈ (DR)DT }
DataHasValue(DPE lt) { x | (x, (lt)LT) ∈ (DPE)DP }
DataMinCardinality(n DPE) { x | #{ y | (x, y) ∈ (DPE)DP} ≥ n }
DataMaxCardinality(n DPE) { x | #{ y | (x, y) ∈ (DPE)DP } ≤ n }
DataExactCardinality(n DPE) { x | #{ y | (x, y) ∈ (DPE)DP } = n }
DataMinCardinality(n DPE DR) { x | #{ y | (x, y) ∈ (DPE)DP and y(DR)DT } ≥ n }
DataMaxCardinality(n DPE DR) { x | #{ y | (x, y) ∈ (DPE)DP and y(DR)DT } ≤ n }
DataExactCardinality(n DPE DR) { x | #{ y | (x, y) ∈ (DPE)DP and y(DR)DT } = n }

A.1.2 Object Property Expressions

The object property interpretation function ·OP is extended to object property expressions as shown in Table 2.

Table 2. Interpreting Object Property Expressions
Object Property Expression Interpretation ·OP
ObjectInverseOf(OP) { (x, y) | (y, x) ∈ (OP)OP }

A.1.3 Data Ranges

The datatype interpretation function ·DT is extended to data ranges as shown in Table 3. All datatypes in OWL 2 are unary, so each datatype DT is interpreted as a unary relation over ΔD — that is, as a set (DT)DTΔD. OWL 2 currently does not define data ranges of arity more than one; however, by allowing for n-ary data ranges, the syntax of OWL 2 provides a "hook" allowing implementations to introduce extensions such as comparisons and arithmetic. An n-ary data range DR is interpreted as an n-ary relation (DR)DT over ΔD — that is, as a set (DT)DTD)n.

Table 3. Interpreting Data Ranges
Data Range Interpretation ·DT
DataIntersectionOf(DR1 ... DRn) (DR1)DT ∩ ... ∩ (DRn)DT
DataUnionOf(DR1 ... DRn) (DR1)DT ∪ ... ∪ (DRn)DT
DataComplementOf(DR) D)n \ (DR)DT where n is the arity of DR
DataOneOf(lt1 ... ltn) { (lt1)LT, ..., (ltn)LT }
DatatypeRestriction(DT F1 lt1 ... Fn ltn) (DT)DT ∩ (F1, lt1)FA ∩ ... ∩ ( Fn, ltn)FA

A.2 Satisfaction of Axioms

A.2.1 Class Expression Axioms

Satisfaction of OWL 2 class expression axioms in Γ with respect to an ontology O is defined as shown in Table 4.

Table 4. Satisfaction of Class Expression Axioms in an Interpretation
Axiom Condition
SubClassOf(CE1 CE2) (CE1)C(CE2)C
EquivalentClasses(CE1 ... CEn) (CEj)C = (CEk)C for each 1 ≤ jn and each 1 ≤ kn
DisjointClasses(CE1 ... CEn) (CEj)C(CEk)C = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
DisjointUnion(C CE1 ... CEn) (C)C = (CE1)C ∪ ... ∪ (CEn)C and
(CEj)C(CEk)C = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk

A.2.2 Object Property Expression Axioms

Satisfaction of OWL 2 object property expression axioms in Γ with respect to an ontology O is defined as shown in Table 5.

Table 5. Satisfaction of Object Property Expression Axioms in an Interpretation
Axiom Condition
SubObjectPropertyOf(OPE1 OPE2) (OPE1)OP(OPE2)OP
SubObjectPropertyOf(ObjectPropertyChain( OPE1 ... OPEn) OPE) y0, ..., yn: ( y0, y1) ∈ (OPE1)OP and ... and ( yn-1, yn) ∈ (OPEn)OP imply (y0, yn) ∈ (OPE)OP
EquivalentObjectProperties(OPE1 ... OPEn) (OPEj)OP = (OPEk)OP for each 1 ≤ jn and each 1 ≤ kn
DisjointObjectProperties(OPE1 ... OPEn) (OPEj)OP(OPEk)OP = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
ObjectPropertyDomain(OPE CE) x, y: (x, y) ∈ (OPE)OP implies x(CE)C
ObjectPropertyRange(OPE CE) x, y: (x, y) ∈ (OPE)OP implies y(CE)C
InverseObjectProperties(OPE1 OPE2 ) (OPE1)OP = { (x, y) | ( y, x) ∈ (OPE2)OP }
FunctionalObjectProperty(OPE) x, y1, y2: ( x, y1) ∈ (OPE)OP and (x, y2) ∈ (OPE)OP imply y1 = y2
InverseFunctionalObjectProperty(OPE) x1, x2, y: ( x1, y) ∈ (OPE)OP and (x2, y) ∈ (OPE)OP imply x1 = x2
ReflexiveObjectProperty(OPE) x: xΔI implies (x, x) ∈ (OPE)OP
IrreflexiveObjectProperty(OPE) x: xΔI implies (x, x) ∉ (OPE)OP
SymmetricObjectProperty(OPE) x, y: (x, y) ∈ (OPE)OP implies (y, x) ∈ (OPE)OP
AsymmetricObjectProperty(OPE) x, y: (x, y) ∈ (OPE)OP implies (y, x) ∉ (OPE)OP
TransitiveObjectProperty(OPE) x, y, z: (x, y) ∈ (OPE)OP and (y, z) ∈ (OPE)OP imply (x, z) ∈ (OPE)OP

A.2.3 Data Property Expression Axioms

Satisfaction of OWL 2 data property expression axioms in I with respect to an ontology O is defined as shown in Table 6.

Table 6. Satisfaction of Data Property Expression Axioms in an Interpretation
Axiom Condition
SubDataPropertyOf(DPE1 DPE2) (DPE1)DP(DPE2)DP
EquivalentDataProperties(DPE1 ... DPEn) (DPEj)DP = (DPEk)DP for each 1 ≤ jn and each 1 ≤ kn
DisjointDataProperties(DPE1 ... DPEn) (DPEj)DP(DPEk)DP = ∅ for each 1 ≤ jn and each 1 ≤ kn such that jk
DataPropertyDomain(DPE CE) x, y: (x, y) ∈ (DPE)DP implies x(CE)C
DataPropertyRange(DPE DR) x, y: (x, y) ∈ (DPE)DP implies y(DR)DT
FunctionalDataProperty(DPE) x, y1, y2: ( x, y1) ∈ (DPE)DP and (x, y2) ∈ (DPE)DP imply y1 = y2

A.2.4 Datatype Definitions

Satisfaction of datatype definitions in Γ with respect to an ontology O is defined as shown in Table 7.

Table 7. Satisfaction of Datatype Definitions in an Interpretation
Axiom Condition
DatatypeDefinition(DT DR) (DT)DT = (DR)DT

A.2.5 Keys

Satisfaction of keys in Γ with respect to an ontology O is defined as shown in Table 8.

Table 8. Satisfaction of Keys in an Interpretation
Axiom Condition
HasKey(CE (OPE1 ... OPEm) ( DPE1 ... DPEn)) x, y, z1, ..., zm, w1, ..., wn:
if x(CE)C and ISNAMEDO(x) and
y(CE)C and ISNAMEDO(y) and
(x, zi) ∈ (OPEi)OP and (y, zi) ∈ (OPEi)OP and ISNAMEDO(zi) for each 1 ≤ im and
(x, wj) ∈ (DPEj)DP and (y, wj) ∈ (DPEj)DP for each 1 ≤ jn
then x = y

A.2.6 Assertions

Satisfaction of OWL 2 assertions in Γ with respect to an ontology O is defined as shown in Table 9.

Table 9. Satisfaction of Assertions in an Interpretation
Axiom Condition
SameIndividual(a1 ... an) (aj)I = (ak)I for each 1 ≤ jn and each 1 ≤ kn
DifferentIndividuals(a1 ... an) (aj)I(ak)I for each 1 ≤ jn and each 1 ≤ kn such that jk
ClassAssertion(CE a) (a)I(CE)C
ObjectPropertyAssertion(OPE a1 a2 ) ((a1)I, (a2)I) ∈ (OPE)OP
NegativeObjectPropertyAssertion(OPE a1 a2) ((a1)I, (a2)I) ∉ (OPE)OP
DataPropertyAssertion(DPE a lt) ((a)I, (lt)LT) ∈ (DPE)DP
NegativeDataPropertyAssertion(DPE a lt) ((a)I, (lt)LT) ∉ (DPE)DP