OWL reasoning: Necessary and sufficient conditions

We are trying to get a reasoner (e.g. HermiT in Protege) to infer that a more specific sub-property can be used instead of the asserted general property.

Classes:

- Patient
- Finding
    - Dyspnea
- ObservationStatus
     - Inclusion
     - Exclusion

Properties:

- has_finding (domain: Patient, range: Finding) 
    - has_positive_finding (domain: Patient, range: Finding, Inclusion)
    - has_negative_finding (domain: Patient, range: Finding, Exclusion)

If we assert the following triples:

:Patient1 a :Patient .
:Patient1 :has_negative_finding :Dyspnea1 .

A reasoner can infer (among other things) that:

:Dyspnea1 a :Finding .
:Dyspnea1 a :Exclusion.

But when we look at it the other way around and assert:

:Patient1 a :Patient .
:Dyspnea1 a :Dyspnea .
:Dyspnea1 a :Exclusion .
:Patient1 :has_finding :Dyspnea1.

We would like the reasoner to infer that:

:Patient1 :has_negative_finding :Dyspnea1 .

We cannot seem to get Protege and HermiT to draw that conclusion and infer the triples.

What are we missing? Are the conditions not necessary and sufficient for it to infer that knowledge?

:Patient1 a :Patient .
:Dyspnea1 a :Dyspnea .
:Dyspnea1 a :Exclusion .
:Patient1 :has_finding :Dyspnea1. 
We would like the reasoner to infer that:
:Patient1 :has_negative_finding :Dyspnea1 .
… What are we missing? Are the conditions not necessary and sufficient for it to infer that knowledge?

There are a few issues here.

First, you haven't said that every has_finding actually corresponds to one of the subproperties. That is, just because something has as finding, you don't know that it also has a negative or a positive finding. The finding could just be a general finding, without being one of the more specific ones.

Second, the more specific type of the object doesn't mean that you have to use the more specific property.

Third, even if you state that the finding is an exclusion, if you don't know that exclusions are disjoint from inclusions, you could still have the finding be both a positive and negative finding.

Now, what it'd be really nice to do would be to state that has_finding is the union of has_negative_finding and has_positive_finding, and then declare inclusion and exclusion disjoint. Then every instance of a finding would have to be one or the other, and you could make your inference.

Since you can't do that, you'll need some sort of alternative. If you're using individuals as per-person diagnoses, then you could say that every finding is either a negative finding or a positive finding with an axiom like

(inverse(hasFinding) some Patient) subClass ((inverse(hasNegativeFinding) some Patient) or (inverse(hasPositiveFinding) some Patient))

along with making hasFinding inverse functional, so that each finding is associated with at most one patient. Then you'd have an ontology like this:

@prefix :      <http://stackoverflow.com/a/30903552/1281433/> .
@prefix a:     <http://stackoverflow.com/a/30903552/1281433/> .
@prefix rdf:   <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix owl:   <http://www.w3.org/2002/07/owl#> .
@prefix xsd:   <http://www.w3.org/2001/XMLSchema#> .
@prefix rdfs:  <http://www.w3.org/2000/01/rdf-schema#> .

a:Exclusion  a           owl:Class ;
        rdfs:subClassOf  a:Finding .

a:hasNegativeFinding  a     owl:ObjectProperty ;
        rdfs:range          a:Exclusion ;
        rdfs:subPropertyOf  a:hasFinding .

_:b0    a                   owl:Restriction ;
        owl:onProperty      a:hasPositiveFinding ;
        owl:someValuesFrom  a:Inclusion .

a:      a       owl:Ontology .

[ a                   owl:Restriction ;
  rdfs:subClassOf     [ a            owl:Class ;
                        owl:unionOf  ( _:b1 _:b0 )
                      ] ;
  owl:onProperty      a:hasFinding ;
  owl:someValuesFrom  a:Finding
] .

a:Finding  a                 owl:Class ;
        owl:disjointUnionOf  ( a:Finding a:Inclusion ) .

a:patient1  a         owl:Thing , owl:NamedIndividual ;
        a:hasFinding  a:dyspnea1 .

_:b1    a                   owl:Restriction ;
        owl:onProperty      a:hasNegativeFinding ;
        owl:someValuesFrom  a:Exclusion .

a:hasFinding  a  owl:ObjectProperty .

a:Inclusion  a           owl:Class ;
        rdfs:subClassOf  a:Finding .

a:hasPositiveFinding  a     owl:ObjectProperty ;
        rdfs:range          a:Inclusion ;
        rdfs:subPropertyOf  a:hasFinding .

a:dyspnea1  a   owl:NamedIndividual , a:Exclusion .

and you can get results like this: