Proof services

The proof services of Evee are defined by the class AbstractProofService (and its extensions), which in turn extends the abstract Protégé class ProofService. These proof services are the access point for Protégé to receive the Evee proofs. To provide a proof service, the most important methods are hasProof and getProof.

The method hasProof is used by Protégé to check if the proof service should be displayed in the drop-down menu of the explanation window. The implementation of this method needs to be very fast in order to avoid slowing down Protégé. To accommodate this, we simply check whether the proof service is enabled in the preferences of Protégé and return this boolean value. If a proof service is enabled, but unable to actually provide a proof, we will display a message to the user in the explanation window.

The method getProof is used to return an object implementing the interface DynamicProof (which is defined in puli). Such an object represents the actual proof that is to be displayed. The proofs that are returned by our proof services are extensions of the class AbstractDynamicProofAdapter. These adapters are used to turn the internal proofs of Evee - which use the interface IProof found in the module evee-data - into a DynamicProof as defined by puli. Right before returning the proof adapter in the method getProof, the method start of the class AbstracDynamicProofAdapter is executed in order to begin computation of the proofs.

The classes that inherit from AbstractProofService are lightweight classes which only call the constructor of the abstract class with the specific dynamic proof adapter for this proof service.