# FullSemanticsSequenceBased

The repaired OWL 1 Full semantics of axioms which receive a sequence as an argument.

Axioms to build unions, intersections, and enumerations have the form of triples with a sequence on their right hand side. The main semantic conditions for the sequence-based axioms was wrongly defined, leading to inconsistency of OWL 1 Full.

## The problem with the main semantic conditions

The following example shows the the original main semantic condition for 'owl:unionOf' axioms in OWL 1 Full:

```   (c,l) ∈ EXT_I(S_I(owl:unionOf))
IF AND ONLY IF
c ∈ IOC,
l is a sequence of d_1, ..., d_n over IOC,
CEXT_I(c) = CEXT_I(d_1) ∪ ... ∪ CEXT_I(d_n)
```

Note that for the ONLY-IF direction the variables d_1, ..., d_n are not mentioned in the antecedent, which allows to interpret them arbitrarily in the consequent. The problem can be characterized more generally by the following "law of prenexity":

``` ( ∀x: A → B(x) ) ↔ ( A → ∀x: B(x) )
```

where the variable x must not occur free in the predicate A. From this, together with the comprehension principles in OWL 1 Full, and by choosing adequate axiomatic triples of RDFS, it is easy see that this leads to inconsistency.

The straightforward repair works by pulling the sequence out of the IFF condition as a "guard":

``` IF
l is a sequence of d_1,...,d_n over IOT
THEN
(c,l) ∈ EXT_I(S_I(owl:unionOf))
IF AND ONLY IF
c ∈ IOC,
d_1, ..., d_n ∈ IOC,
CEXT_I(c) = CEXT_I(d_1) ∪ ... ∪ CEXT_I(d_n)
```

Below, I have defined repairing semantics for the main semantic condition of all sequence based axioms.

## Unions

### Syntax

``` c owl:unionOf SEQ(d_1 ... d_n)
```

### Semantics

Axiomatic triples (existing in OWL 1 Full):

``` owl:unionOf rdf:type owl:ObjectProperty
```

Axiomatic triples (missing in OWL 1 Full):

``` owl:unionOf rdfs:domain owl:Class
owl:unionOf rdfs:range rdf:List
```

Repaired main semantic condition:

``` IF
l is a sequence of d_1,...,d_n over IOT
THEN
(c,l) ∈ EXT_I(S_I(owl:unionOf))
IF AND ONLY IF
c ∈ IOC,
d_1, ..., d_n ∈ IOC,
CEXT_I(c) = CEXT_I(d_1) ∪ ... ∪ CEXT_I(d_n)
```

Comprehension principle:

``` IF
l is a sequence of d_1, ..., d_n over IOC
THEN ∃ c:
c ∈ IOC,
(c,l) ∈ EXT_I(S_I(owl:unionOf))
```

## Intersections

### Syntax

``` c owl:intersectionOf SEQ(d_1 ... d_n)
```

### Semantics

Axiomatic triples (existing in OWL 1 Full):

``` owl:intersectionOf rdf:type owl:ObjectProperty
```

Axiomatic triples (missing in OWL 1 Full):

``` owl:intersectionOf rdfs:domain owl:Class
owl:intersectionOf rdfs:range rdf:List
```

Repaired main semantic condition:

``` IF
l is a sequence of d_1,...,d_n over IOT
THEN
(c,l) ∈ EXT_I(S_I(owl:intersectionOf))
IF AND ONLY IF
c ∈ IOC,
d_1, ..., d_n ∈ IOC,
CEXT_I(c) = CEXT_I(d_1) ∩ ... ∩ CEXT_I(d_n)
```

Comprehension principle:

``` IF
l is a sequence of d_1, ..., d_n over IOC
THEN ∃ c:
c ∈ IOC,
(c,l) ∈ EXT_I(S_I(owl:intersectionOf))
```

## Enumerations

Note: Only the part of the semantics, which is analogue to the semantics of unionOf and intersectionOf is treated here. For a complete treatment of the semantics of enumerations, see FullSemanticsOneOf.

### Syntax

``` c owl:oneOf SEQ(y_1 ... y_n)
```

### Semantics

Axiomatic triples (existing in OWL 1 Full):

``` owl:oneOf rdf:type owl:ObjectProperty
```

Axiomatic triples (missing in OWL 1 Full):

``` owl:oneOf rdfs:domain owl:Class
owl:oneOf rdfs:range rdf:List
```

Repaired main semantic conditions:

``` IF
l is a sequence of y_1,...,y_n over IOT
THEN
(c,l) ∈ EXT_I(S_I(owl:oneOf))
IF AND ONLY IF
c ∈ IOC,
CEXT_I(c) = { y_1, ..., y_n }
```
``` IF
l is a sequence of y_1,...,y_n over LV_I
(c,l) ∈ EXT_I(S_I(owl:oneOf))
THEN
c ∈ IDC,
CEXT_I(c) = { y_1, ..., y_n }
```

Comprehension principles:

``` IF
l is a sequence of y_1, ..., y_n over IOT
THEN ∃ c:
c ∈ IOC,
(c,l) ∈ EXT_I(S_I(owl:oneOf))
```
``` IF
l is a sequence of y_1, ..., y_n over LV_I
THEN ∃ c:
c ∈ IDC,
(c,l) ∈ EXT_I(S_I(owl:oneOf))
```