Abduction non entailment services

A non-entailment explanation service using abduction provides explanations for non-entailments in the form of sets of hypotheses. Each hypothesis is a set of axioms, s.t. by adding the hypothesis to the ontology, the missing entailment becomes entailed. Each explanation service using abduction hooks into the extension point de.tu_dresden.inf.lat.evee.nonEntailment_explanation_service defined in evee-protege-core.

Evee currently provides two non-entailment explanation services. The first one uses the abduction solver LETHE and is contained in the plugin evee-protege-abduction-lethe, the second one uses the FOL theorem prover SPASS and is contained in the plugin evee-protege-abduction-capi. Note that the service of the plugin evee-protege-abduction-capi relies on the external module capi-java-component, which is contained in the directory lib of Evee, since this module is currently not made public via maven.

The page Abstract Abduction Solver provides information on an abstract abduction solver class that can be extended by non-entailment explanation services using abduction.

The page Result manager and result display provides information on how the UI of the computed explanations is created.

The page LETHE abduction solver provides information on the non-entailment explanation service using abduction which relies on LETHE for its internal computation.

The page CAPI abduction solver provides information on the non-entailment explanation service using abduction which relies on the FOL theorem prover SPASS for its internal computation.