Warning:
This wiki has been archived and is now read-only.

FullSemanticsQCRs

From OWL
(Redirected from FullSemanticsQCR)
Jump to: navigation, search

Goto OWL 2 Full Semantics Page


The OWL 2 Full semantics of Qualified Cardinality Restrictions (QCRs).

Note: The RDF syntax of QCRs has been changed to the current form by resolving Issue 122.

Axiomatic Triples

Axiomatic triples, derived from OWL 1 Full: see page on axiomatic triples.

 owl:qualifiedCardinality rdf:type rdf:Property
 owl:qualifiedCardinality rdfs:domain owl:Restriction
 owl:qualifiedCardinality rdfs:range xsd:nonNegativeInteger
 owl:minQualifiedCardinality rdf:type rdf:Property
 owl:minQualifiedCardinality rdfs:domain owl:Restriction
 owl:minQualifiedCardinality rdfs:range xsd:nonNegativeInteger
 owl:maxQualifiedCardinality rdf:type rdf:Property
 owl:maxQualifiedCardinality rdfs:domain owl:Restriction
 owl:maxQualifiedCardinality rdfs:range xsd:nonNegativeInteger
 owl:onClass rdf:type rdf:Property
 owl:onClass rdfs:domain owl:Restriction
 owl:onClass rdfs:range owl:Class 
 owl:onDataRange rdf:type rdf:Property
 owl:onDataRange rdfs:domain owl:Restriction
 owl:onDataRange rdfs:range rdfs:Datatype

Exact Qualified Object Cardinality Restrictions

Syntax

 x rdf:type owl:Restriction
 x owl:onProperty p
 x owl:qualifiedCardinality "n"^^xsd:nonNegativeInteger
 x owl:onClass c

Semantics

Main semantic condition:

 IF
   (x,n) ∈ EXT_I(S_I(owl:qualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onClass))
 THEN
   x ∈ IOR,
   n ∈ LV_I, n is a non-negative integer,
   p ∈ IOOP,
   c ∈ IOC,
   CEXT_I(x) = { u | card({v | (u,v) ∈ EXT_I(p) ∧ v ∈ CEXT_I(c)}) = n }
   

Comprehension principle:

 IF
   p ∈ IOOP,
   n ∈ LV_I, n is a non-negative integer,
   c ∈ IOC
 THEN ∃ x:
   x in IOR,
   (x,n) ∈ EXT_I(S_I(owl:qualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onClass))

Exact Qualified Data Cardinality Restrictions

Syntax

 x rdf:type owl:Restriction
 x owl:onProperty p
 x owl:qualifiedCardinality "n"^^xsd:nonNegativeInteger
 x owl:onDataRange c

Semantics

Main semantic condition:

 IF
   (x,n) ∈ EXT_I(S_I(owl:qualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onDataRange))
 THEN
   x ∈ IOR,
   n ∈ LV_I, n is a non-negative integer,
   p ∈ IODP,
   c ∈ IDC,
   CEXT_I(x) = { u | card({v ∈ LV_I | (u,v) ∈ EXT_I(p) ∧ v ∈ CEXT_I(c)}) = n }
   

Comprehension principle:

 IF
   p ∈ IODP,
   n ∈ LV_I, n is a non-negative integer,
   c ∈ IDC
 THEN ∃ x:
   x in IOR,
   (x,n) ∈ EXT_I(S_I(owl:qualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onDataRange))

Min Qualified Object Cardinality Restrictions

Syntax

 x rdf:type owl:Restriction
 x owl:onProperty p
 x owl:minQualifiedCardinality "n"^^xsd:nonNegativeInteger
 x owl:onClass c

Semantics

Main semantic condition:

 IF
   (x,n) ∈ EXT_I(S_I(owl:minQualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onClass))
 THEN
   x ∈ IOR,
   n ∈ LV_I, n is a non-negative integer,
   p ∈ IOOP,
   c ∈ IOC,
   CEXT_I(x) = { u | card({v | (u,v) ∈ EXT_I(p) ∧ v ∈ CEXT_I(c)}) ≥ n }
   

Comprehension principle:

 IF
   p ∈ IOOP,
   n ∈ LV_I, n is a non-negative integer,
   c ∈ IOC
 THEN ∃ x:
   x in IOR,
   (x,n) ∈ EXT_I(S_I(owl:minQualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onClass))

Min Qualified Data Cardinality Restrictions

Syntax

 x rdf:type owl:Restriction
 x owl:onProperty p
 x owl:minQualifiedCardinality "n"^^xsd:nonNegativeInteger
 x owl:onDataRange c

Semantics

Main semantic condition:

 IF
   (x,n) ∈ EXT_I(S_I(owl:minQualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onDataRange))
 THEN
   x ∈ IOR,
   n ∈ LV_I, n is a non-negative integer,
   p ∈ IODP,
   c ∈ IDC,
   CEXT_I(x) = { u | card({v ∈ LV_I | (u,v) ∈ EXT_I(p) ∧ v ∈ CEXT_I(c)}) ≥ n }
   

Comprehension principle:

 IF
   p ∈ IODP,
   n ∈ LV_I, n is a non-negative integer,
   c ∈ IDC
 THEN ∃ x:
   x in IOR,
   (x,n) ∈ EXT_I(S_I(owl:minQualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onDataRange))

Max Qualified Object Cardinality Restrictions

Syntax

 x rdf:type owl:Restriction
 x owl:onProperty p
 x owl:maxQualifiedCardinality "n"^^xsd:nonNegativeInteger
 x owl:onClass c

Semantics

Main semantic condition:

 IF
   (x,n) ∈ EXT_I(S_I(owl:maxQualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onClass))
 THEN
   x ∈ IOR,
   n ∈ LV_I, n is a non-negative integer,
   p ∈ IOOP,
   c ∈ IOC,
   CEXT_I(x) = { u | card({v | (u,v) ∈ EXT_I(p) ∧ v ∈ CEXT_I(c)}) ≤ n }
   

Comprehension principle:

 IF
   p ∈ IOOP,
   n ∈ LV_I, n is a non-negative integer,
   c ∈ IOC
 THEN ∃ x:
   x in IOR,
   (x,n) ∈ EXT_I(S_I(owl:maxQualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onClass))

Max Qualified Data Cardinality Restrictions

Syntax

 x rdf:type owl:Restriction
 x owl:onProperty p
 x owl:maxQualifiedCardinality "n"^^xsd:nonNegativeInteger
 x owl:onDataRange c

Semantics

Main semantic condition:

 IF
   (x,n) ∈ EXT_I(S_I(owl:maxQualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onDataRange))
 THEN
   x ∈ IOR,
   n ∈ LV_I, n is a non-negative integer,
   p ∈ IODP,
   c ∈ IDC,
   CEXT_I(x) = { u | card({v ∈ LV_I | (u,v) ∈ EXT_I(p) ∧ v ∈ CEXT_I(c)}) ≤ n }
   

Comprehension principle:

 IF
   p ∈ IODP,
   n ∈ LV_I, n is a non-negative integer,
   c ∈ IDC
 THEN ∃ x:
   x in IOR,
   (x,n) ∈ EXT_I(S_I(owl:maxQualifiedCardinality)),
   (x,p) ∈ EXT_I(S_I(owl:onProperty)),
   (x,c) ∈ EXT_I(S_I(owl:onDataRange))

Considerations

  • The range of the cardinality properties has been set to xsd:nonNegativeInteger. This will lead to formal inconsistency of an ontology, which uses cardinality numbers from other number spaces such as xsd:integer. This is a well known problem.
  • Checked generally for cardinality restrictions (TF Action 34): It is not a problem to have "n is a non-negative integer" in the consequent of the main semantic condition.

Goto OWL 2 Full Semantics Page