## 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 .
```

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

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: