CAPI abduction solver

General

The class CapiAbductionSolver provides a non-entailment explanation service using abduction. Internally, the FOL theorem prover SPASS is used for the computation and the auxiliary library capi-java-component is used for pre- and post-processing. CapiAbductionSolver extends the class AbstractAbductionSolver and implements the interface Supplier to provide the required result streams. The abduction result that is saved to the internal caching mechanism is provided as a List containing Solutions (a class found in the capi-java-component). The caching is done via a map containing OWLOntologies as keys and objects of the class AbductionCache<List<Solution>> as values.

Computation of explanations is only possible if the user set the path to the SPASS executable, i.e. SPASS or SPASS.exe, depending on the operating system. If no path is set, a dialog window is opened and the user is asked to provide the path to the executable. Alternatively, the path can be set in the preferences. The internal SPASS solver is able to provide explanations as long as exactly one SubClassOf axiom is entered as a missing entailment.

The actual computation is done by:

1. Creating a separate input file that the SPASS theorem prover can read.
2. Running SPASS on this input file by creating and starting a new process. This generates a new output file.
3. Converting the generated SPASS output file to objects of the class Solutions (of capi-java-component).
4. Returning the generated results as a stream.
5. Cleaning up the temporary files created for and by SPASS.

All files created during this process are saved to a temporary directory provided by the operating system.

Note that SPASS is not part of the bundle evee-protege-abduction-capi and needs to be installed separately by the user. Further information on SPASS can be found here. The capi-java-component, which is required by the CapiAbductionSolver, is contained in Evee as a local repository in the directory lib. All neccessary files of capi-java-component are bundled into the plugin.

Preferences

The capi abduction service comes with its own preferences UI, which is created by the class CapiPreferencesUI. As usual, this class extends Protégé class OWLPreferencesPanel and hooks into the extension point de.tu_dresden.inf.lat.evee.nonEntailment_preferences defined in evee-protege-core. The preferenes are:

1. The path to the SPASS executable
2. The computation time given to the theorem prover SPASS.
3. An option to remove redundancies in solutions.
4. An option to simplify conjunctions in solutions.
5. An option to sort solutions by semantic minimality.