Explaining inconsistent ontologies

[maphih]

@koopmann @tofr961c

Protégé has a special facility for explaining inconsistent ontologies (Reasoner -> Explain inconsistent ontology), which is also implemented by protege-proof-explanation via showing proofs for ⊤⊑⊥. This fails for all of our proof generators because HermiT throws an InconsistentOntologyException. Can this be fixed in some way? Otherwise, we need to implement something to tell protege-proof-explanation that our ProofServices do not support this kind of explanation.@koopmann @tofr961c
Protégé has a special facility for explaining inconsistent ontologies (Reasoner -> Explain inconsistent ontology), which is also implemented by protege-proof-explanation via showing proofs for ⊤⊑⊥. This fails for all of our proof generators because HermiT throws an InconsistentOntologyException. Can this be fixed in some way? Otherwise, we need to implement something to tell protege-proof-explanation that our ProofServices do not support this kind of explanation.

Patrick Koopmann
31 May 2022
This should in theory be fixable, but needs a bit more time. In theory, the elimination proofs and the LETHE-based proofs should use the empty signature as target in this case. However, in addition we might need some additional work: 1. I think explaining inconsistencies has to be done a bit differently when using the OWL API - I remember problems on this from before, 2. LETHE, and I think also FAME, use syntactic module extraction, which requires the ontology to be consistent. Module extraction is not needed at all in our case, since we already extract the justifications, but we have to avoid that the forgetters try to extract a module, 3. at least LETHE assumes the input to be consistent. For example, if at some point the empty clause is derived, it would throw an exception, but there could be other places in the code where I silently assume that the current clause set is consistent.

For now, I think we should give a warning to the users. Next time I have time for this, however, I should have a go and figure out how to make this work.

Stefan Borgwardt
31 May 2022
Given the way protege-proof-explanation works, for now, we should return false for hasProof(⊤⊑⊥).

Tom Friese
3 Jun 2022
this was implemented today (commit 3e19017 in the github-repo)

Patrick Koopmann
6 Jul 2023
As this is non-trivial, I would say for now we should keep the current solution.