Contents

  1. Test Cases
    1. SubPropertyOf OneOf
    2. student/employee
    3. Patel-Schneider Paradox
    4. Cyclic Restriction
    5. Specialised Restriction
  2. Approaches
    1. Daml+Oil Model Theory
    2. Daml+Oil Axiomatic
    3. 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.

Approaches

Daml+Oil Model Theory

Understood in conjunction with dark triples that do not have meaning in the RDF layer.

See:

Daml+Oil Axiomatic

Characterised by the meaning of syntax being indirectly conveyed. Visible in the axiomatic semantics of Daml+OIL, and in RDFS model theory.

See: