FullSemanticsIffExpressions

Goto OWL 2 Full Semantics Page

Work in progress

The expressivity of the OWL 2 Full semantics of boolean class expressions and enumerations.

OWL 1 Full had IFF conditions for all the boolean class expressions and for enumerations. I suggest to only have normative ONLY-IF conditions, and make the sufficient conditions non-normative, by adding them to "Comprehension Principles" section. In order to make the correspondence theorem work, the definition of a "balanced ontology" would need to be extended to also take named class expressions into account, but this is straightforward.

The Problem

NEEDS FURTHER CONSIDERATIONS

In OWL 1 Full, the comprehension principles were not sufficient to proof the correspondence theorem. For example, without the sufficient conditions for union class expressions, the OWL DL entailment G_1 |= G_2 would be an OWL Full non-entailment for the following graphs:

 G_1 := { 
     ex:c rdf:type owl:Class
 }

 G_2 := {
     ex:c rdf:type owl:Class
     ex:c owl:unionOf (SEQ ex:c ex:c)
 }

The reason is as follows.

The OWL Full semantics would definitely provide the following semantic relationships:

 I(ex:c) in IC ,
 ICEXT(I(ex:c)) = ICEXT(I(ex:c)) | ICEXT(I(ex:c))

But since there are no sufficient conditions, we cannot "step up" to G_2.

The comprehension principle for union class expressions would not help by providing the following triples:

 G_CP := {
     _:x owl:unionOf (SEQ ex:c ex:c)
     _:x rdf:type owl:Class   // by further entailment
 }

This would lead to the existence of some x in IR, with: of a mapping B : blank(G_2) -> IR, with

 EXISTS x in IR:
     x in IC ,
     I(ex:c) in IC ,
     ICEXT(x) = ICEXT(I(ex:c)) | ICEXT(I(ex:c))

This would be sufficient to infer the following:

 {
    ex:c owl:equivalentClass _:x
    _:x rdf:type owl:Class 
    _:x owl:unionOf (SEQ ex:c ex:c)
 }  

Rational for Change

• Just as in the case of the comprehension principles, the sufficient conditions are only required in OWL 1 Full to deal with certain aspects of the RDF mapping. There is no real logic related reason for having them: If the RDF mapping was different, then the conditions would be either not necessary, or they would be different.

• Both the purpose and the logical form of the sufficient conditions is very similar to those of the comprehension principles. The sufficient conditions are sort of comprehension principles for named class expressions. (Actually, the only difference is that the comprehension principles explicitly provide for some individual with the class extension of the expression, where the sufficient conditions require such an individual to exist).

• If the RDF mapping in OWL 1 would have been as in OWL 2, the sufficient conditions would be redundant, i.e. the comprehension principles would be sufficient.

• The RDF mapping in OWL 2 only supports the old "named" mappings for backwards compatibility.

• The correspondence theorem of OWL 2 is not dependent on the sufficient conditions.

• Most probably, there will not be a problem with any existing tools (only of interest for "complete" OWL Full reasoners, triple-rule based reasoners don't apply sufficient rules).

• The implementation burden might be high; in any case, it looks like an unnecessary burden on implementers for "more complete" OWL Full reasoners.

• Putting the sufficient conditions to the list of non-normative comprehension principles will still keep them alive, and implementers MAY try to implement them, or approximate them, just as with the comprehension principles.

• Putting the sufficient conditions to the list of non-normative comprehension principles would pretty well match the new strategy.

Goto OWL 2 Full Semantics Page