Skip to content

Dynamic proof adapter

Jump to bottom
maphih edited this page Sep 5, 2025 · 1 revision

Abstract dynamic proof adapter

In order for a proof to be displayed by the plugin protege-proof-explanation, it needs to implement the interface DynamicProof of the plugin puli. This interface is implemented by the class AbstractDynamicProofAdapter.

The AbstractDynamicProofAdapter (and its extensions) are responsible for starting the computation of the actual proof, for providing place-holder inferences and showing a loading screen during the computation, and for updating the proof shown in the explanation window once the computation is complete.

During the construction of an abstract dynamic proof adapter, an object of class AbstractEveeProofPreferencesManager and an object of class EveeDynamicProofLoadingUI need to be provided. The actual extensions of the abstract proof adapter are fairly lightweight. However, before any proofs are computed, they need to ensure the following:

  1. The 'inner proof generator' needs to be set. This proof generator is responsible for the actual computation of the proof. Setting this proof generator is done via the method setInnerProofGenerator of the class AbstractDynamicProofAdapter. Such an inner proof generator needs to implement the interface IProofGenerator of evee-data.
  2. A caching proof generator needs to be created. Such a caching proof generator is a wrapper for the inner proof generator and provides a caching mechanism for the proofs. The functionality to create such a caching proof generator is already implemented in the class AbstractDynamicProofAdapter by the method 'resetCachingProofGenerator'.

Additionally, the extensions of AbstractDynamicProofAdapter can override the method setProofGeneratorParameters, which is responsible for checking whether any preferences were changed by the user. This is necessary to reset the caching proof generator and provide the user with a proof that adheres to the currently specified preferences. In the abstract dynamic proof adapter, this method is only used to check whether the provided signature has changed since the last time a proof was computed. The extensions of AbstractDynamicProofAdapter additionally check whether any of the preferences they support were changed since the last time a proof was computed.

Extensions of the abstract dynamic proof adapter

The abstract proof adapter is extended by the AbstractEveeSuboptimalDynamicProofAdapter, which adds functionality to handle the loading screen for suboptimal proofs. Furthermore, the abstract dynamic proof adapter is extended by the EveeElkBasedDynamicProofAdapter, which is used in the "ELK proof" plugins, and by the EveeLetheBasedDynamicProofAdapter, which is used in the "Detailed proof (LETHE)" plugin. The abstract suboptimal dynamic proof adapter is extended by the different versions of the "Elimination Proof (FAME)" plugins and by the different versions of the "Elimination Proof (LETHE)" plugins. These extensions only differ in the way they create and parametrize their underlying proof generators.

Dynamic proofs and separate threads

All these proof adapters are "dynamic", meaning that they allow for registering a ChangeListener (an interface which is provided by puli). Originally, this interface was created to update a proof in case the ontology is changed while an explanation window is displayed to the user. However, we are also using this feature in order to account for the long computation times of some of our proof services.

In order for the actual proof to be displayed to the user, the dynamic proof adapter implements the method getInferences, which hands a collection of Inference objects (which is another interface of puli) to Protégé. When the computation of a proof is started, this method at first only returns "placeholder inferences", constructed via the method createPlaceholderInference. These tell the user that the proof is currently being computed. Additionally, we display a loading screen during this time. Once the computation of the proof is finished, we update the displayed inferences, either with an error message in case that no proof could be computed, or with the actual inference steps of the proof. The inferences created by the proof generators of Evee implement the interface IInference (found in evee-data). We use the lightweight class EveeInferenceAdapter to turn these into inferences that can be used by Protégé.

The actual computation of the proofs is done in a separate thread, in order to avoid slowing down any user interaction while the proof is generated. This thread is created at the end of the method start, which is executed whenever the method getProof in the class AbstractEveeProofService is called. While the new thread is running, the object of class EveeDynamicProofLoadingUI (which was handed to the abstract dynamic proof adapter during construction) displays a loading screen to the user.

Communication between the new thread object and the dynamic proof adapter is handled through the interface IExplanationGenerationListener (found in evee-data), which is implemented by the dynamic proof adapter. Through the method handleEvent of this interface, the dynamic proof adapter can be informed of the result of the computation in the new thread or of any errors that occur during computation. This method receives an object of class ExplanationEvent (found in evee-protege-core) as its only parameter. This explanation event has a source and a type. The source is an object implementing the interface IExplanationGenerator (found in evee-data). In our case, this interface is implemented by the thread object itself. The type is an enum ExplanationEventType (found in evee-protege-core) and is used to determine the nature of the event occurring in the thread. Currently, the following types are supported by the dynamic proof adapter:

  • COMPUTATION_COMPLETE
  • COMPUTATION_CANCELLED
  • ERROR
  • NOT_SUPPORTED

The last one of these types is necessary because at the time when the method getProof is called in the proof service, it is not yet clear if our proof generators are actually able to provide a proof for the entailment. This can only be checked later, once the proof generation has actually started.

Clone this wiki locally