Create an option to dump a list of explanations for unsatisfiable classes

[cmungall]

A complement to #174

Analogous owltools option: -e or run-reasoner command. owltools dumps a flat list of axioms in the explanation rendering IRIs as IRI-label pairs.

For robot, it would be super-awesome to have something similar, but more user friendly

• ability to render as markdown, for easy pasting into tickets (I have made probably 100s of github tickets with protege UI explanation screenshots, which are not very searchable)
• use of nesting, as in the Protege explanation UI
• option to render source ontology(s) of each axiom [v useful for debugging where an errant import is often to blame]

Protege will find all explanations but will allow you to interrupt its search. I personally think the choice of explanation is abitrary and would be happy for the tool to include just one.

• Maybe an option to find max N.

• Bonus: in an ontology with multiple unsats, it can be useful to start with the one with the most minimal explanation, typically the MRCAs of all unsats in the asserted hierarchy. It may even be possible to combine explanations to find the most likely offending axiom.

• Bonus bonus: plug in kboom to use probabilistic OWL inference to find the most likely overall resolution...

I believe @matentzn is working on something like this. I am neutral as to whether this is part of robot or a separate dependency on maven central that robot can include.

[balhoff]

ability to render as markdown, for easy pasting into tickets

This would be awesome.

option to render source ontology(s) of each axiom

Would be nice as a title attribute to show as tooltip (not sure how to do that in markdown). Protege is supposed to show this but it seems to have broken a while back (the tooltips claim all the axioms have source "inferred").

[beckyjackson]

Does the explain command meet this request?

[balhoff]

I think this could reuse the functionality in ExplainOperation, but it would be a little more specific. It would need to get the list of unsatisfiable classes "Xs" and then ask for the explanation for each axiom of the form X EquivalentTo owl:Nothing. This could potentially be thousands of computations and very slow, so adding an algorithm to guess at the most general problem class would probably be important. So, I think there is more work to do before closing this.

[cmungall]

not sure what you mean, I do this manually in Protege all the time, the first explanation is always fine

[balhoff]

I mean what you wrote in your “bonus” above. We can take just one explanation for each, but I frequently see thousands of unsatisfiable classes at once.

[matentzn]

FYI The algorithm for computing the most general unsatisfiable classes is called root unsatisfiable classes; https://www.sciencedirect.com/science/article/pii/S1570826805000260
https://pdfs.semanticscholar.org/87f3/7150aedbfd59b772241081ef81edc1249158.pdf
Maybe there even is something in the @matthewhorridge explanation framework that does it by now.

[balhoff]

Nice, thanks @matentzn!

[matthewhorridge]

There is some – possibly shoddy ;) – code in the explanation package for computing root/derived unsatisfiable classes. See this interface and this implementation.

I do recall there being some basic problems with original definitions of root/derived unsatisfiable classes but, right now, I'm struggling to remember the exact problems, other than that they were broken. I also can't find my notes from 10 years ago. I think the formal definition, that was couched in terms of justifications, was broken as I came up with some counter examples. If I think of them, I'll post them.

[matentzn]

I would like to mention that I would be veeeery interested in this ticket to be implemented. I am currently faced with huge ontologies and unsats all the time, and I would like a way I can dump a random (ideally root) justification for x unsatisfiable classes as markdown (some parameter to say: dump unsat explanations, if any, and another to restrict the number, in case there are thousands).

[matentzn]

@balhoff and I have implemented most of what this ticket is asking for now in #779

I wont consider the kboom request as part of this ticket, but I will do the "source ontology" one.

[beckyjackson]

I believe #779 resolved this, but please reopen if you need.