The trigger was working out an example that Philippe tried to do at
the OBI workshop.
Consider this ontology:
Namespace(ex = <http://example.com/>)
Ontology(<http://example.com/> Class(ex:manuf_role partial ex:role )
Individual(ex:affy type(ex:organization ))
ObjectProperty(ex:has_role )
ObjectProperty(ex:is_manufactured_by range(restriction(ex:has_role
someValuesFrom(ex:manuf_role ))))
Class(ex:hg133 partial ex:microarray )
Class(ex:hg133 partial restriction(ex:is_manufactured_by value
(ex:affy )))
Class(ex:manufacturer complete restriction(ex:has_role
someValuesFrom(ex:manuf_role ))))
I would expect that ex:affy would be classified as a ex:manufacturer.
I am wrong. In order to have this work one needs to add an an
explicit microarray individual:
Individual(ex:hg133i1 type(ex:hg133 ))
I had wrongly expected that a reasoner would assume there exists a
instance of every class *at the same time*. In fact the
satisfiability checked are done by asserting at least one instance of
each class exists *serially*.
Here's another example:
(defun maybe-not ()
(with-ontology maybe ()
((class !owl:Thing :partial (one-of !a !b))
(class !c1 :partial !owl:Thing)
(class !c2 :partial !owl:Thing)
(class !c3 :partial !owl:Thing)
(disjoint-classes !c1 !c2 !c3))
(print-db (check maybe))
)
(with-ontology not ()
((class !owl:Thing :partial (one-of !a !b))
(class !c1 :partial !owl:Thing)
(class !c2 :partial !owl:Thing)
(class !c3 :partial !owl:Thing)
(individual (type !c1))
(individual (type !c2))
(individual (type !c3))
(disjoint-classes !c1 !c2 !c3))
(print-db (check not))
))
There is no complaint about the first ontology (nor should there be)
but the second is caught as problematic.
From a realist point of view, all classes have instances, in
parallel. (OWL terminology: coherent, jointly-satisfiable)
My inclination is to suggest that OBI - and the OWL versions of all
OBO ontologies - declare anonymous individuals of each type named in
the ontology. (actually having them for the leaf classes ought to be
adequate). I'd have this scripted, as it would be a pain to maintain
otherwise.
This would both ensure that the type of entailment that Philippe and
I assumed happen, would reliably happen, and that "incoherent"
ontologies were detected.
-Alan
Interesting... I too am surprised by this and was surprised when the example would not infer. Are you suggesting adding instance to the releases of OBI then, i.e. after the merging scripts have been ran?