Support for sorting and disabling proof services

[stefborg]

This addresses #2, but depends on protegeproject/protege#1059 since it uses a configuration option from the general explanation preferences (and also reuses the utility class SortedPluginsTableModel).

I tested this with the proof services from https://github.com/liveontologies/elk-reasoner and https://github.com/de-tu-dresden-inf-lat/evee.

[stefborg]

I applied the same fix as for the Protege ExplanationManager, so that the proof services should be reloaded properly when resetting the preferences.

[ykazakov]

Thanks for the update! I will probably copy the SortedPluginsTableModel to the plugin so that it works also for old versions of Protege. If there is no configuration options for the default explanation option, I would assume that the most recently used plugin should be used first (the previous behaviour).

Just out of curiosity: why did you implement many versions of the "Elimination Proof" plugin instead of just one plugin with many options? Or perhaps two plugins for "FAME" and "LETHE"?

[stefborg]

I don't recall all the implementation details, but at least we only have two JARs (one for FAME and one for LETHE). The different variants are provided as separate ProofServices, but each of those is only a relatively lightweight wrapper around a core AbstractEveeProofService. We wanted to have them as separate ProofService extensions, so that one can easily choose among all available proof options in the proof service list provided by protege-proof-explanation.

[ykazakov]

We wanted to have them as separate ProofService extensions, so that one can easily choose among all available proof options in the proof service list provided by protege-proof-explanation.

Do you mean in preferences or in the explanation window for a particular entailment? In the explanation window you can easily expose all options using an third-level dropdown menu. See, e.g., Fig. 4. here.

I am asking because currently it is not possible to set a priority like FAME proofs < Justification Explanations < LETHE proofs, and I am not certain that something like that could be useful, and if so, how it could be realised in the UI.

[stefborg]

Do you mean in preferences or in the explanation window for a particular entailment? In the explanation window you can easily expose all options using an third-level dropdown menu. See, e.g., Fig. 4. here.

I think we specifically discussed this and decided against a nested drop-down menu, to have all options visible at the same time (at least all proof-based explanations). This would also require implementing a new priority management for each nested level of services.

I am asking because currently it is not possible to set a priority like FAME proofs < Justification Explanations < LETHE proofs, and I am not certain that something like that could be useful, and if so, how it could be realised in the UI.

At least between LETHE and FAME, this is now possible with this PR. Of course, it would be easier if there were only one top-level "LETHE proof service" and one "FAME proof service". However, for us, the biggest concern was to put the faster proof services at the top of the priority list (to make sure that the first proof is computed quickly), i.e. an order like "LETHE < FAME < LETHE size-optimized < FAME size-optimized ...". This would not be so easily possible if they were grouped into "LETHE" and "FAME" services.

Having an order like "FAME < Justifications < LETHE" is not possible right now, and would be very hard to do unless we convert all proof services into explanation services, right?

[ykazakov]

Having an order like "FAME < Justifications < LETHE" is not possible right now, and would be very hard to do unless we convert all proof services into explanation services, right?

Right now, yes, but before making the final decision for priority management in Protege, I wanted to understand the use cases.

In theory, it is possible to implement a very flexible priory management in the following way:

• upgrade the method hasExplanation(OWLAxiom) of ExplanationService so that the result is a non-negative number. The value 0 would then mean the same as false before, but with a positive number one could let the plugin to estimate how well it could explain the given axiom.
• sort all explanation services according to these values in the dropdown-menu when explaining a particular axiom
• if an explanation plugin (like proof-explanations) has several options (plugins), it could delegate calculating these values by taking the minimum over hasProof(OWLAxiom) for these options/plugins.
• a default priority for each explanation service can be set in preferences (as a number).

In particular, for the scenario "Fame < Justifications < Lethe", one assigns the default priority of Proofs, say, to 3, and Justifications, say to 5 (can be provided as default values by each plugin). Then in the settings for Proofs, one assigns to Fame the priority of 10. With these settings, if all 3 variants can explain an axiom, the first selected option will be Proofs > Fame. If Fame is not applicable, the selected option is Justifications, etc. In principle, one can display these numbers also in this drop-down menu for better clarity.

From the user point of view, the settings may be more complicated to use (one needs to come up with numbers not just sort plugins), but overall, this approach seems more flexible.

A more advanced setup could, in theory, assign priorities according to statistics about execution times for proof services, which could be measured like for reasoning tasks (see Preferences > Reasoner > Displayed inferences).

[stefborg]

There are two aspects you mentioned: (1) automatically computed priorities and (2) user-defined subjective priorities. They seem to be more or less independent, except that user-defined numbers would override the automatically computed ones.

For (1), we would need a clear semantics of what these numbers mean. Otherwise, how could we compare a 10 returned by one plugin to a 100 returned by another?

For (2), I agree that it is more flexible, but also much more complicated for the user. Say I want to have the order "Fame < Justifications < Lethe < Fame optimized < Lethe optimized". Now I have to manually assign 5 numbers to each of these services, on several different preference panels. Then later I want to insert a new proof method between Justification and Lethe, and I may have to assign completely new numbers to every service (unless I left sufficiently large gaps between the numbers).

Since all that counts in the end is the order of these numbers anyway, I think it makes sense to use an interface that directly reflects this order, e.g. a. list. To be able to order all explanation services, we could think about making ProofService derive from ExplanationService (or something similar), so that every proof service can be directly included in the Protege explanation panel and sorted there (together with justifications). We would then also need to adapt the explanation dialog, if we want to keep the functionality of allowing to group explanation services into "Proofs", "Elimination proofs", etc.

[ykazakov]

My point is that by assigning number priorities to services and sub-services one can achieve any ordering of explanation options. The usability aspects (what these numbers mean and how to enter them) should of course be considered as well.

Note that the flat view of all explanations is also not an ideal solutions either. Let's say we prioritised all proof explanations over all justification explanations, and then we decided to do that the other way round. That would mean that we need to move lots of entries in the list. Besides, if each combination of options (e.g., ELK proofs with "inline inferences" but without "Remove unnecessary inferences") results in a new entry in the list, this would quickly blow up the list size. That is why I was puzzled why you needed to create many variants of the Fame and Lethe plugins instead of providing just two base plugin with user-selectable options.

To be able to order all explanation services, we could think about making ProofService derive from ExplanationService (or something similar), so that every proof service can be directly included in the Protege explanation panel and sorted there (together with justifications).

Well, explanation plugins need to be instantiated by some manager, and I do not think that ExplanationManager should be responsible for instantiating proof-based explanations: we do not want ELK proof explanation services to be instantiated if the proof-explanation-plugin is not installed, for otherwise we get ClassNotFound exceptions.

But something along this line is clearly possible. For example, we could require an ExplanationPlugin to return not just one ExplanationService (using newInstance()) but a list of ExplanationServices, for all possible combination of plugin options. Then such methods can be delegated from plugins to plugins. For example, if a ProofPlugin returns a list of ProofServices, the proof-explanation manager can wrap each of these services to an ExplanationService and return the resulting list in its implementation of ExplanationPlugin. However, as I mentioned, I am not convinced that this is a good idea from the usability point of view as it could make the list of ExplanationServices very very long.

[stefborg]

Let's say we prioritised all proof explanations over all justification explanations, and then we decided to do that the other way round. That would mean that we need to move lots of entries in the list.

The same happens in your approach, if the user already assigned numbers to the individual proof and justification services. For the list view, we could think of a bulk selection mode for this use case, e.g. using the Shift key, which I think would be quite intuitive.

Besides, if each combination of options (e.g., ELK proofs with "inline inferences" but without "Remove unnecessary inferences") results in a new entry in the list, this would quickly blow up the list size. That is why I was puzzled why you needed to create many variants of the Fame and Lethe plugins instead of providing just two base plugin with user-selectable options.

Yes, the number of entries is problematic, but we tried to keep them low, and offer the less important options only in the preferences. The reason is that we want to be able to switch proof options for each individual explained axiom. For one axiom, "LETHE" may give a better proof, for another one "optimized LETHE". I wouldn't want to go to the preferences each time I want to see a different proof format. If the list becomes too long, we can definitely think about grouping options in another combo box.

[ykazakov]

The same happens in your approach, if the user already assigned numbers to the individual proof and justification services.

Not to the same degree: changing a number is easier than moving an entry over multiple positions. But I agree that, in general, sometimes one may need to change lots of things, which is unsurprising given that one can represent exponentially-many different orderings.

I wouldn't want to go to the preferences each time I want to see a different proof format.

I see. Please take a look at our JustificationComputationService. There we have applied a more general approach where a service can also manage preferences for individual entailments which are then displayed in the explanation window. See the definition of JustificationComputationManager, specifically the function getSettingsPanel(). Would something like that be of interest to your proof explanation plugins? If so, we could discuss a similar extended definition of a proof service.

[ykazakov]

So actually I was wrong here, currently it is not possible to add a third-level menu for proof-based explanations:

In the explanation window you can easily expose all options using an third-level dropdown menu. See, e.g., Fig. 4. here.

Note from the definition of JustificationComputationManager that the settings does not have to be a combo-box. It can essentially be any panel like for general preferences.

[stefborg]

I see. Please take a look at our JustificationComputationService. There we have applied a more general approach where a service can also manage preferences for individual entailments which are then displayed in the explanation window. See the definition of JustificationComputationManager, specifically the function getSettingsPanel(). Would something like that be of interest to your proof explanation plugins? If so, we could discuss a similar extended definition of a proof service.

That would actually be very useful for us, and it would also alleviate the problems with the high number of proof services. We should probably discuss this in a separate issue. I think the high-level sorting and disabling of proof services (i.e. this PR) is still useful even if there are fewer services, e.g. to always show the ELK proof first (if there is one).

[ykazakov]

OK, let's continue the discussion regarding preferences in #4.