ENVO is outside DL profile which causes reasoners to fail #1072
Comments
|
actually there are many more
action items
When introducing complex axioms into ENVO we need to be careful, and need to balance complexity vs the gains. Do these cardinality axioms buy us anything, either in terms of entailments, error checking, or elucidating the ontology I will also add this to my document on why it's a good idea to be very careful when using complex OWL axioms |
cmungall
changed the title
|
I started writing a note about how to fix this, but this has happened often enough across multiple ontologies I generalized it into a blog post: https://douroucouli.wordpress.com/2021/03/24/avoid-mixing-parthood-with-cardinality-constraints/ |
|
Update:
|
…02220>); it made the ontology incoherent; see https://github.com/EnvironmentOntology/envo/issues/1072\#issuecomment-807735583
|
Update:
|
|
The weakening of these axioms in the associated PR has tossed out essential distinctions. I want most of them back in. If we can't use complex / non-simple properties, then we need simple ones to do the same job. has component and has component process were brought up in this vein. We'd need similar relations for adjacent to and overlaps but I don't see any non-simple characteristics on that property - why do those cause errors? Thanks @cmungall for the blog post, very useful. But I'm getting rapidly bored with the OBO attitude of "that's just how we do it" - that's the sort of thing that leads to the regrettable |
|
This was causing the ontology to be inconsistent. So, I removed the functional assertion, which appears to have been a mistake. See details here: #1073 (comment) |
|
A lot to unpack here. Starting with the basics:
See @wdduncan's comment. There is no reason to create a non-transitive version of adjacent, because adjacent is not transitive anyway. It was incorrectly declared as a Functional property in ENVO, this was clearly an error. It was corrected in this PR because the problem was only uncovered once we fixed the ontology so HermiT would run.
Note we cannot add the axioms back in without reverting the ontology to its broken state. I will have @wdduncan substitute the original axioms using has-component in place of has-part. This is a distinct state of affairs from adding the original axioms back in, there are nuanced differences, and there are potential traps here. It is quite possible that the essential distinctions use case you have in mind will not be satisfied by using non-transitive subproperties. I could help best here if the reasons why you feel it is essential to have these logical axioms in the ontology are documented somewhere. But for now, in the interests of moving forward, @wdduncan, can you substitute the original axioms for analogous ones with component relations?
There are many things that should be OBO documentation. However, this documentation is expensive to produce and there is not enough funding, resources, and expertise to make all the documentation we would like. This is also competing with resources to improve tooling across OBO (and non-OBO ontologies), which is also expensive. The expense is significantly compounded by the desire of each individual ontology to do things slightly differently. (Arguably, this particular piece of documentation is lower priority as the W3C OWL2 specs document what can and cannot be in an OWL profile; and we have also had documentation on has-component for some time, and exemplar uses) Nevertheless, I am committed to creating cross-OBO documentation that satisfies everyone. There is a process here though. I can't just take my blog post and bless it as OBO documentation. We have to reach consensus on what are priorities, what are problems needing fixed, and what the recommended solution or solutions are - often accompanied by tooling support. For many of these, we should also be engaging the community beyond OBO, and I always try and do that where possible. But please recognize this is a very expensive, time consuming process. This is particularly challenging for cases such as this one. The tradeoffs and costs are nuanced and often require a lot of OWL expertise to understand. This is made more difficult by undocumented reasoner use cases (beyond the usual ones of classification and error checking). My strategy is to first document the problem based on personal experience with a blog post; sometimes informal so I don't lose key audience members (perhaps sometimes too informal or too opinionated, I will accept). Even if these do not advance to formal recommendations of the OBO group, I find that these are still incredibly helpful. I can point people at them so they can at least get some basic background in the problem. The vast majority of the time these save me and other ontology developers a lot of time, resources, and serve to nip potentially costly problems in the bud. I would like to advance this particular recommendation further, but please be patient. The process will need to take into account voices such as yours, who disagree with the recommendation to avoid component relations. It may be the case that the majority agree with you on this and the eventual OBO recommendation will be to use the component relations. Or perhaps there are other potential solutions others may want to take into consideration. My blog post is just the start of a process here.
I'm not totally sure what you are referring to here. My blog post was my own perspective on the problem and my own recommended fix, not the opinion of OBO. And I agree that has-component is confusing. But I think you would prefer that to the alternative leaving cardinality assertions out altogether? And I am not totally sure how the has-component relation arose from an attitude of "that's just how we do it". It was added for people to optionally use precisely to avoid the DL profile restriction.
I am not sure if you are referring to the hasDbXref or synonym properties. If the former, I agree 100%. If the latter I may not understand the proposal. But let's make a separate ticket for this. |
|
Since ENVO now satisfies with the DL profile, I am closing this issue. The addition of the |
|
I am reopening this as adding a full ro import (#1182) has revealed there are additional DL violations. The problems are with the has-participant relation For example:
I am afraid these axioms have to go. I know you don't want to remove these axiom @pbuttigieg but to stress again, this is not my decision, I did not have a hand in the OWL spec, if I did I would definitely allow these axioms. But I didn't, and here we are. As with the analogous has-part case the only solution is to introduce a fake object property that is a subproperty of has-participant. Unlike has-part, we do not have such a fake relation predefined in RO. I suggest that in order to expedite this, we create a subproperty of has-participant in ENVO and use this object property in the QCR axioms. Do you have any suggestions on how to name this @dosumis? My preferred plan is to remove the QCRs altogether and keep simple existential axioms, but if the QCRs are serving a purpose then I think the plan above is the only one open to us |
|
Should we add the simple has participant relation to RO? Suggestions for what to call the relation:
|
|
Cardinalities could be handled in a SHACL or ShEX layer on top of the OWL. |
|
@dr-shorthair - I am a big fan of shape languages (in most of my projects we use linkml and compile down to shex) However, I don't think that is what is desired here. Unless I misunderstand @pbuttigieg's goals, the intent is not to make a closed world schema for validating information being exchanged, but it is to make an open-world OWL ontological-realist model of the world. In practical terms, it should be possible to use envo to communicate an abox with an instance of an interplate earthquake, without passing the names of two tectonic plates. See https://douroucouli.wordpress.com/2020/09/04/the-open-world-assumption-considered-harmful/ (despite the provocative title, I like the OWA, it's just important to use OW modeling when that is the intent, and CW when that is the intent) |
|
@wdduncan - if you can get a RO release out quickly sure. But I regard this as a matter of urgency, and would rather get a new ENVO release out first of the 3 choices I prefer the 2nd one. Another option is has-direct-participant, somewhat analogous to has-component, it is still v hard to get a non-fuzzy definition |
|
@cmungall Another possible option is to annotate the axioms. For instance suppose, we add annotation properties (I'm not tied to these names):
We could annotate then annotate the axiom Reasoning will ignore the annotation. But that is okay. Is it too hacky? Too confusing? |
|
Or perhaps use a single
|
|
Yes indeed. I'm a big fan of not losing information, by putting it in annotations, even when axiomatization has to be removed due to OWL profile limitations. |
|
I like the annotation idea. But you don't need to repeat the name of the property as it's there in the annotated axiom I would just mirror the owl predicates as APs, e.g you would annotate the axiom with minCardinaliti with value 2 |
|
I included the name of the property in order to account for cases in the axioms have more than one property. E.g.: |
|
so equivalence axioms may have more than one OP, but you can't make the equivalence axioms with the weaker clauses :-) Another not uncommon scenario would be nesting, e.g. A sub P some Q some Y. I usually eschew these but there are a handful in ENVO I would opt to keep it simple and cover the 99%. A comment can always be added for another @pbuttigieg what do you think? |
|
@cmungall sorry ... I'm not quite following your point :) Suppose we a class has a subclass axiom like: If we simply add the annotation Does 'min 2' refer to the whole axiom? |
Ah, that's an expression not an axiom So that expression could be used with any OWL axiom type, but realistically there are not many scenarios where this would not be SC or EC If you have a SC axiom A SubClassOf ('part of' some Foo) and ('has input' some Bar) We would of course write this as two axioms, never as one. There is discussion elsewhere in this issue tracker about this That leaves EC and my point above was that it wouldn't be correct to weaken an equivalence axiom with QCRs and to replace them with SVFs (unless the EC axiom was wrong in the first place) |
|
The original issue was filed half a year ago Let's just get a release out that fixes the OWL Change the QCRs to SVFs in SC axioms, just stick an rdfs:comment on the axiom with controlled natural language that states the intent. We can always refine later. Agreed @pbuttigieg ? |
|
where do we stand on this @wdduncan? |
|
Yeah, it bites me too on my releases.. |
|
I always considered undeclared declarations irrelevant if types can be inferred by the serialiser. In ODK, this is what we do: https://github.com/pato-ontology/pato/blob/master/src/ontology/Makefile#L138 The serialisation to OFN basically automatically adds the declarations all by itself, so all the errors go away. |
|
@matentzn Sorry, I'm not following. See attached for errors. |
|
@matentzn To be clear: there isn't a make command to convert |
|
You are right, sorry.. Maybe this was caused by some intermediate step. See here for a potential fix: https://github.com/EnvironmentOntology/envo/pull/1307/files |
|
Thanks @matentzn ! PR #1307 did the trick :) Here is the output: |
|
This issue will be closed when we document the outcome and SOP for handling cardinality etc in the ENVO wiki |
When HermiT is used to reason over http://purl.obolibrary.org/obo/envo/releases/2020-06-10/envo.owl (current release), there are errors of the form:
The reason for this is HermiT doesn't let you use cardinality constraints with non-simple object properties (i.e., object properties for which a characteristic such
Transitivehas been defined). ELK happily ignores such things :)In the case of the specific error above, the error is due to this:
However, there are other examples, such as
biomehas the axiom:Not sure how we missed this before now ...
cc @cmungall
The text was updated successfully, but these errors were encountered: