# FullSemanticsAxiomaticTriples

WORK IN PROGRESS

Axiomatic triples in OWL 1 Full.

The RDF(S) semantics spec includes a list of so called "axiomatic triples" for the RDF(S) vocabulary.

Note: I regard the omission of axiomatic triples for OWL Full as a bug. So I am going to introduce the missing axiomatic triples for OWL Full in this page. Additional axiomatic triples for OWL 2 Full are specified together with their respective language features.

## Example Axiomatic Triples in RDFS

Examples for axiomatic triples are

``` rdfs:subClassOf rdfs:domain rdfs:Class
rdf:type rdf:type rdf:Property
rdfs:Class rdfs:subClassOf rdfs:Resource
rdfs:isDefinedBy rdfs:subPropertyOf rdfs:seeAlso
```

These axiomatic triples correspond to the following model-theoretic semantic conditions, which are characterized by not containing bound variables, and not having an antecedent:

``` (S_I(rdfs:subClassOf), S_I(rdfs:Class)) ∈ EXT_I(S_I(rdfs:domain))
S_I(rdf:type) ∈ CEXT_I(S_I(rdf:Property))
CEXT_I(S_I(rdfs:Class)) ⊆ CEXT_I(S_I(rdfs:Resource))
EXT_I(S_I(rdfs:isDefinedBy)) ⊆ EXT_I(S_I(rdfs:seeAlso))
```

The axiomatic triples of RDF(S) are true in every RDF(S)-ontology, in particular they are part of the entailment closure of the empty RDF graph. OWL Full does not provide a systematic collection of axiomatic triples for the OWL specific vocabulary, although some axiomatic triples can be identified by investigating the different tables containing the semantic conditions of OWL Full.

## A Design Principle

In OWL Full (old and new version) the following relationships hold:

``` CEXT_I(S_I(owl:Thing)) = CEXT_I(S_I(rdfs:Resource))
CEXT_I(S_I(owl:Class)) = CEXT_I(S_I(rdfs:Class))
CEXT_I(S_I(owl:ObjectProperty)) = CEXT_I(S_I(rdf:Property))
```

However, it might be confusing to see for example that the range of owl:equivalentProperty is owl:ObjectProperty, where it is allowed to have such axioms also with instances of owl:DataProperty. So in these "polimorphic" cases, the more general looking class from RDFS is used.

This has the additional advantage, that this approach would not conflict with an RDFS based OWL DL language, as it was defined for OWL 1 in section 5.4 of the AS&S.

## Missing axiomatic triples

### Missing axiomatic triples for classes

While there are axiomatic triples for all classes in the OWL vocabulary, for some of them it makes sense to have stricter semantics. This is true for all property characteristics classes, which are only specified to be classes, instead of being subclasses of at least rdf:Property. In the case of symmetric and transitive properties, the formally more specific class owl:ObjectProperty is used, since this gives a hint to the intended usage.

``` owl:FunctionalProperty rdfs:subClassOf rdf:Property
```
``` owl:InverseFunctionalProperty rdfs:subClassOf rdf:Property
```
``` owl:SymmetricProperty rdfs:subClassOf owl:ObjectProperty
```
``` owl:TransitiveProperty rdfs:subClassOf owl:ObjectProperty
```

### Missing axiomatic triples for properties

The 2nd paragraph in the list "OWL built-in syntactic classes and properties" only specify typing axioms of the form "p type Property". There is no domain or range given for these properties. In many cases it is not possible to entail these missing axiomatic triples. In those cases where it is actually possible (e.g. for owl:sameAs), the domain and range has been added anyway for completeness and convenience.

#### Individual axiom vocabulary

The semantics for owl:sameAs and owl:differentFrom is specified to be equivalent to = and ≠, respectively. These are global relations, being specified everywhere on rdfs:Resource. This means that the following axiomatic triples can actually be entailed. They have been added, anyway, for convenience and completeness.

``` owl:sameAs rdfs:domain rdfs:Resource
owl:sameAs rdfs:range rdfs:Resource
```
``` owl:differentFrom rdfs:domain rdfs:Resource
owl:differentFrom rdfs:range rdfs:Resource
```
``` owl:distinctMembers rdfs:domain owl:AllDifferent
owl:distinctMembers rdfs:range rdf:List
```

#### Class axiom vocabulary

``` owl:equivalentClass rdfs:domain owl:Class
owl:equivalentClass rdfs:range owl:Class
```
``` owl:disjointWith rdfs:domain owl:Class
owl:disjointWith rdfs:range owl:Class
```

#### Class description vocabulary

``` owl:complementOf rdfs:domain owl:Class
owl:complementOf rdfs:range owl:Class
```
``` owl:unionOf rdfs:domain owl:Class
owl:unionOf rdfs:range rdf:List
```
``` owl:intersectionOf rdfs:domain owl:Class
owl:intersectionOf rdfs:range rdf:List
```
``` owl:oneOf rdfs:domain rdfs:Class
owl:oneOf rdfs:range rdf:List
```

#### Property axioms vocabulary

owl:equivalentProperty can be applied both on data properties and on object properties. To avoid confusion we use here rdf:Property instead of owl:ObjectProperty.

``` owl:equivalentProperty rdfs:domain rdf:Property
owl:equivalentProperty rdfs:range rdf:Property
```
``` owl:inverseOf rdfs:domain owl:ObjectProperty
owl:inverseOf rdfs:range owl:ObjectProperty
```

#### Restriction vocabulary

Restrictions can be applied to data properties and object properties, so rdf:Property is used here. AllValues and SomeValues restrictions can be applied both on object classes and datatypes, so rdfs:Class is used here. HasValue restrictions restrictions can be applied both on individuals and on datavalues, so rdfs:Resource is used here.

``` owl:onProperty rdfs:domain owl:Restriction
owl:onProperty rdfs:range rdf:Property
```
``` owl:allValuesFrom rdfs:domain owl:Restriction
owl:allValuesFrom rdfs:range rdfs:Class
```
``` owl:someValuesFrom rdfs:domain owl:Restriction
owl:someValuesFrom rdfs:range rdfs:Class
```
``` owl:hasValue rdfs:domain owl:Restriction
owl:hasValue rdfs:range rdfs:Resource
```
``` owl:cardinality rdf:type rdf:Property
owl:cardinality rdfs:domain owl:Restriction
owl:cardinality rdfs:range xsd:NonNegativeInteger

owl:minCardinality rdf:type rdf:Property
owl:minCardinality rdfs:domain owl:Restriction
owl:minCardinality rdfs:range xsd:NonNegativeInteger
```
``` owl:maxCardinality rdf:type rdf:Property
owl:maxCardinality rdfs:domain owl:Restriction
owl:maxCardinality rdfs:range xsd:NonNegativeInteger
```

### Missing axiomatic triples for individuals

There are no missing axiomatic triples for individuals, see below.

## Non-missing axiomatic triples

### Non-Missing axiomatic triples for classes

For all classes which are not property characteristics classes, there are sufficient axiomatic triples in OWL Full.

• For all the classes in the "parts" table there is at least one of a typing axiom and a subclass axiom (or both).
• There are redundant axiomatic triples: "owl:Class subClassOf rdfs:Class" entails "owl:Class type rdfs:Class".
• Some axiomatic triples are repetitions from RDFS, e.g. "rdfs:Datatype subClassOf rdfs:Class"
• The axiomatic triple for 'owl:DatatypeProperty' is "DatatypeProperty subClassOf ObjectProperty". This can be seen from the "Characteristics" table, where it is stated that the property extension of a DatatypeProperty is a subset of IOTxLV_I, which is a subset of IOTxIOT. Via the IFF semantics of rdfs:subClassOf one receives the claimed axiomatic triple as an entailment.
• For the classes owl:DeprecatedClass and owl:DeprecatedProperty it is stated in the "built-in" list that they are just rdfs:Class. This is sufficient.

### Non-Missing axiomatic triples for properties

• The annotation properties in OWL:
• owl:versionInfo, rdfs:label, rdfs:comment, rdfs:seeAlso, rdfs:isDefinedBy
• All are of "type owl:AnnotationProperty" according to list "OWL built-in syntactic classes and properties" ("are all in IOAP")
• All have a domain and range according to "Characteristics" table: domain(ap) = range(ap) = owl:Thing ("EXT_I(p) subset IOTxIOT")
• The ontology properties:
• owl:imports, owl:priorVersion, owl:backwardCompatibleWith, owl:incompatibleWith
• All are of "type owl:OntologyProperty" according to list "OWL built-in syntactic classes and properties" ("are all in IOXP")
• All have a domain and range according to "Characteristics" table: domain(ap) = range(ap) = owl:Ontology ("EXT_I(p) subset IXxIX")

### Non-Missing axiomatic triples for individuals

There are no individuals in the OWL vocabulary, which are neither classes nor properties.