LETHE abduction solver

The class LetheAbductionSolver provides a non-entailment explanation service using abduction. Internally, LETHE is used for the computation. LetheAbductionSolver 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 an object of the class DLStatement (of LETHE). The caching is done via a map containing OWLOntologies as keys and objects of the class AbductionCache<DLStatement> as values.

Before starting the computation, the service starts a new thread object, which sleeps for ten seconds and then updates the message displayed in NonEntailmentExplanationLoadingScreenManager via the progress tracker. This is done because the internal LETHE abduction solver cannot estimate the remaining computation time. The message is therefore simply updated to inform the user of a longer waiting time and to suggest changing the vocabulary.

The internal LETHE solver is able to provide explanations as long as some missing entailment (not necessarily a SubClassOf axiom) and some Permitted Vocabulary are provided. The filtering of the ontology is done internally by LETHE itself. The information whether axioms were ignored is then forwarded to the NonEntailmentViewComponent once the computation is completed.

DLStatements can represent infinitely many solutions - depending on the specific ontology, missing entailment and vocabulary. These solutions need to be unraveled before they can be displayed to the user. This unraveling is done by mimicking a breadth-first-search through a tree of solutions, where each branch has (potentially) infinite length. This is done in the method get which is part of the interface Supplier that is used to provide the result streams.