Fixed order of proof services

[stefborg]

Hello!

We are using this plugin for multiple proof services that generate different kinds of proofs. However, some of these methods are slower than others. When clicking on "?" in Protege, it seems that a random proof service is chosen at first, which is inconvenient if that one takes very long to produce a proof.

Have you already considered a way of specifying a priority order between proof services? What would be the best way to integrate this here? We could also help with the implementation.

Best,
Stefan

[ykazakov]

Usually Protege selects the last used explanation service. Are you saying that this is not the case for proof-based explanations? This should be easy to fix.

What exactly do you mean by priority? The order in which the services should be displayed in the drop-down menu? I guess, it might be possible to allow the user to change the order in preferences for proof-based explanations. However, I cannot change the order of explanation plugins (the top level drop down list) because this is controlled by the explanation workbench.

[stefborg]

Yes, we are only interested in the proof services, not the top-level dropdown list. But it is not enough to just change the order in the list (although that would also be nice to have).

What I meant is that we want to fix the order of proof services that are asked to produce a proof whenever someone clicks on "?", e.g. "always try Service1 first, and use Service2 only if Service1 did not return a proof". Selecting the last used service is not good in the scenario where Service1 is fast but may produce "ugly" proofs, Service2 is slow but produces "nicer" proofs. In this case, I always want to use Servive1 first to get a first proof fast, and only use Service2 if I am interested in a better proof (or Service1 failed for some reason).

[ykazakov]

What I meant is that we want to fix the order of proof services that are asked to produce a proof whenever someone clicks on "?", e.g. "always try Service1 first, and use Service2 only if Service1 did not return a proof".

What do you mean by "Service 1 did not return a proof"? Do you suggest that the plugin should run Service 1 with some timeout and if the timeout is exceeded, then run Service 2 automatically?

As mentioned, the proof explanation plugin just mimics the behaviour of the explanation workbench, which always selects the last used service and does not run multiple services automatically. If we are to modify this behaviour for proof explanations, I think, this should also be done accordingly in the explanation workbench. Indeed, the scenario you have described can be also imagined with general explanation services: e.g., the user may want first to try computing justifications, and if it takes too much time (e.g., because there are exponentially-many justifications), display the proofs, or other kinds of explanations.

What if we allow setting the "default explanation service", either to the "last used" (by default) or some fixed service from the list? In the scenario that you have described, if the default explanation service does not work well, the user may choose other services from the drop menu. In this case, I am not sure that changing the order of services in the list is really necessary since the lists should not be very long. But some stable order (e.g., an alphabetical) may be useful.

Another thing to consider: currently the API is such that the list of available services depends on the chosen axiom. See here:

protege-proof-explanation/src/main/java/org/liveontologies/protege/explanation/proof/ProofBasedExplanationService.java

Line 58 in 67e35d0

public boolean hasExplanation(OWLAxiom axiom) {

If the default service is not on the list, one has to decide which other service to take. For this reason, maybe a better solution is to allow changing the order of services and then setting the default service to either "last used" or "first available" (which is also chosen if the last used is not available).

[stefborg]

Yes, your last solution sounds perfect. As you said, this should be made consistent across all plugins in the explanation workbench.

By "Service 1 did not return a proof" I actually meant what you said, i.e., that Service1 may not support the target axiom, and then the next service in the list is selected automatically.

If we would not allow changing the order of the list, then it could still be the case that the first service takes very long and blocks the whole explanation workbench, so the user cannot even select a different option. (For this reason, we have included a progress bar and cancellation functionality in some of our proof services.)

Where would be the best place to start implementing this?

[ykazakov]

By "Service 1 did not return a proof" I actually meant what you said, i.e., that Service1 may not support the target axiom, and then the next service in the list is selected automatically.

Just out of curiosity, how do you decide that your proof service does not support the axiom? Hopefully, you do not perform any expensive computation (e.g., trying to compute the proof) during the call of the method that should decide it?

protege-proof-explanation/src/main/java/org/liveontologies/protege/explanation/proof/service/ProofService.java

Line 81 in 67e35d0

public abstract boolean hasProof(OWLAxiom entailment);

If so, this is not a good idea. The implementation of this method should be cheap. If possible, the decision should be made just by a syntactical check. The reason is that this method is used to check wether the ? button should be displayed next to axiom, and this check can be executed many times for many axioms, even without much user interaction. For example, this check is performed for every axiom displayed in the Protege window, and also repeated every time when the window is repainted, e.g., as a result of mouse move or resize (however, this value may be cached). Try it for yourself: just remove all other explanation plugins except for this one.

To sum up: this is not the method intended to work around incompleteness! If the proof service is not guaranteed to return a proof (and this cannot be checked fast) then the method should return yes. Then if there is no proof, the explanation will simply be empty:

protege-proof-explanation/src/main/java/org/liveontologies/protege/explanation/proof/list/ProofRoot.java

Line 42 in 67e35d0

static final String NO_PROOF = "No proof for the entailment found.";

This is not our invention, a similar method should be implemented by any explanation plugins:

protege-proof-explanation/src/main/java/org/liveontologies/protege/explanation/proof/ProofBasedExplanationService.java

Line 58 in 67e35d0

public boolean hasExplanation(OWLAxiom axiom) {

[stefborg]

Yes, we had already noticed this but did not know why exactly hasProof was called so often. Thank you for the explanation! We will try to avoid doing anything expensive there.

[ykazakov]

Where would be the best place to start implementing this?

• Add "up" and "down" buttons to change the order of plugins in the general preference panel:
  

  protege-proof-explanation/src/main/java/org/liveontologies/protege/explanation/proof/preferences/ProofBasedExplanationPreferencesGeneralPanel.java

  Line 96 in 67e35d0

  private void addInstalledProofServicesComponent(

• Add an option (e.g., radio buttons) for setting the Default explanation service among two options:
  • Last used (if available) [selected by default]
  • Frist available in the list
• Persist these settings so that they are preserved when Protege restarts
  https://github.com/liveontologies/protege-proof-explanation/blob/67e35d0c574ca14405f2228ac34e41960bcb954c/src/main/java/org/liveontologies/protege/explanation/proof/preferences/ProofBasedExplPrefs.java
• Use the settings to return the plugins in the desired order by the ProofManager
  

  protege-proof-explanation/src/main/java/org/liveontologies/protege/explanation/proof/ProofManager.java

  Line 242 in 67e35d0

  public Collection<ProofService> getServices() {

• Select the default plugin according to the settings:
  

  protege-proof-explanation/src/main/java/org/liveontologies/protege/explanation/proof/ProofBasedExplanationResult.java

  Line 118 in 67e35d0

  proofManager_.selectService(services[0]);

Pull requests are welcomed! ;-)

[ykazakov]

Actually the settings for the Default explanation service should probably be moved to Protege explanation preferences.
See here: protegeproject/protege#653