Contents

  1. Test Cases
    1. SubPropertyOf OneOf
    2. student/employee
    3. Patel-Schneider Paradox
    4. Circular Restriction
    5. Specialised Restriction
    6. List Ontology
  2. Approaches
    1. Dark Owl
    2. Dark Lists
    3. Daml+Oil Axiomatic
    4. Axiomatic + Comprehension
  3. Comparison

Test Cases

SubPropertyOf OneOf

Premise
foo rdfs:subPropertyOf daml:oneOf .
_:eg foo _:list .
_:list daml:rest daml:nil .
_:list daml:first _:singleton .
_:list rdf:type daml:List .
Conclusion
foo daml:sameInstanceAs _:singleton .
Intermediate Point
_:eg  daml:oneOf _:list .
_:list daml:rest daml:nil .
_:list daml:first _:singleton .
_:list rdf:type daml:List .

All the solutions accept that the intermediate point entails the conclusion. Hence, those that deny that the premise entails the solution also deny that the premise entails (at the WebOnt level) the intermediate point.

student/employee

Premise
John rdf:type Student .
John rdf:type Employee .
Conclusion
John rdf:type _:i .
_:i rdf:type daml:Class .
_:i daml:intersectionOf _:l .
_:l rdf:type daml:List .
_:l daml:first Student .
_:l daml:rest _:t .
_:t rdf:type daml:List .
_:t daml:first Employee .
_:t daml:rest daml:nil .

Patel-Schneider Paradox

Premise
Deliberately empty
Conclusion
_:1 rdf:type owl:Restriction .
_:1 owl:onProperty rdf:type .
_:1 owl:maxCardinalityQ "0" .
_:1 owl:hasClassQ _:2 .
_:2 owl:oneOf _:3 .
_:3 owl:first _:1 .
_:3 owl:rest owl:nil .
_:1 rdf:type _: 1 .

All of the solutions must reject the self inconsistent conclusion. The question is why do they reject it. (Using the disputed status of the maxCardinalityQ property is cheating).

Circular Restriction

See circular primitive

Premise
John child John .
Conclusion
John rdf:type _:1 . 
_:1 rdf:type daml:Restriction . 
_:1 rdf:onProperty child . 
_:1 rdf:hasClass :_1 .

Specialised Restriction

Premise
RestrictionOnParent owl:subClassOf owl:Restriction .
RestrictionOnParent owl:subClassOf _:x .
_:x rdf:type owl:Restriction .
_:x owl:onProperty owl:onProperty .
_:x owl:hasValue parent .

_:z rdf:type RestrictionOnParent .
_:z owl:hasValue foo .

_:a rdf:type _:z .
Conclusion
_:a parent foo .
Intermediate Form
_:z rdf:type owl:Restriction .
_:z owl:hasValue foo .
_:z owl:onProperty parent .

_:a rdf:type _:z .

Once again, all the systems agree that the intermediate form entails the conclusion. So the issue is whether the intermediate form is entailed by the premise.

List Ontology

Premise
_:a owl:first _:b .
_:r rdf:type owl:Restriction .
_:r owl:onProperty owl:first .
_:r owl:hasValue owl:Thing .
Conclusion
_:a rdf:type _:r .

More generally we can imagine using owl to specify the uniquess constraints etc that characterise being a list. Would such an activity have the intended effect; or is it not supported.

Approaches

Dark Owl

DAML+OIL, particularly as expressed in the DAML+OIL model theory, understood in conjunction with all daml triples being dark triples that do not have meaning in the RDF layer.

See:

Dark lists

DAML+OIL, particularly as expressed in the DAML+OIL model theory, understood as respecting RDFS model theory, except that the triples constructing daml:Lists are dark and do not have meaning in the RDF layer. Understood that implicit triples count in the mapping from syntactic construct to semantic constraint.

See:

Daml+Oil Axiomatic + Explicit Comprehension

Characterised by explicit axioms saying which DAML Classes exist. The meaning of syntax is indirectly conveyed. Visible in the axiomatic semantics of Daml+OIL, and in RDFS model theory.

See:

Daml+Oil Axiomatic, without comprehension

Characterised by the meaning of syntax being indirectly conveyed. Visible in the axiomatic semantics of Daml+OIL, and in RDFS model theory.
Lacks comprehension, i.e. DAML Classes which you may want to talk about using a class expression do not necessarily exist.

See:

Comparison

Dark Owl Dark Lists DAML+OIL
with comprehension		 DAML+OIL
w/o comprehension
Champion Peter Pat Jeremy no-one
subPropertyOf no yes? yes yes
student/employee yes no? yes no
paradox no
Inconsistent.		 no
No comprehension at all.		 no
Not entailed by axioms.		 no
No comprehension at all.
circular yes no yes no
specialised
restriction		 no yes yes yes
list onto no no yes yes

Another key point of comparison is whether the layering is consistent with mathematical principles, that each layer is defined on the previous layer and is not self-referential, or with computer science style, where each layer may have significant self-reference (eat your own dog food, minimum fixed point semantics?). The dark proposals typically reduce the amount of permitted self reference.