# FullSemanticsQCRs

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.