Skip to content

Preferences manager

maphih edited this page Sep 5, 2025 · 1 revision

The EveeProofPreferencesManager is responsible for loading and saving preferences so that they can be re-used in later Protégé-executions. These preferences can be changed by the user and are accessible in the preferences window of Protégé under File -> Preferences -> Explanations -> Proofs.

Since the Evee proof services use different proof generators with different properties, there are four different versions of the preference manager:

  1. The general proof preferences manager (AbstractEveeProofPreferencesManager), which provides the functionality to enable and disable proof services.
  2. The suboptimal proof preferences manager (AbstractEveeSuboptimalProofPreferencesManager), which extends the general proof preferences manager. This preferences manager provides additional functionality to show a Suboptimal proof warning if the computation was cancelled before an optimal proof could be found. The preferences manager allows switching between showing the warning and not showing the warning.
  3. The elimination proof preferences manager (AbstractEveeEliminationProofPreferencesManager), which extends the suboptimal proof preferences manager. This preferences manager provides additional functionality to use the internal Protégé reasoner instead of the HermiT reasoner (currently not supported by the underlying proof generators), to merge several proof steps into one, and to vary justifications.
  4. The signature proof preferences manager (AbstractEveeSignaturePreferencesManager). This preferences manager provides functionality to use a signature in the proofs in order to hide certain proof steps.

When constructing an object that extends the AbstractEveeProofPreferencesManager, a setId, a preferenceId and a proofServiceName need to be provided. While setId and preferenceId are internal values that are only used to save information to the Protégé preferences, the proofServiceName is additionally also used to display the name of the proof service to the user in the preferences window.

Note that each class extending the AbstractEveeDynamicProofAdapter actually has two preferences managers: One is either a general, suboptimal, or elimination preferences manager (depending on which functionalities the proof generator of this adapter supports), the other is a signature preferences manager.

Clone this wiki locally