protegeproject / explanation-workbench Goto Github PK

If I press (?) next to a stated axiom, e.g., NammedPizza SubClassOf Pizza in the pizza ontology, I get the empty explanation.

Clearly, the explanation should be not empty as this axiom is not a tautology.

When people click on the explanation for why owl:Nothing is a subclass of a given class, or owl:Thing is a superclass of a given class, a dialog pops up generating and endless list of results. People get confused by this, and not knowing what is going on, they often just kill Protégé. Would be much better to treat these cases differently and give a more concise and more easily interpretable explanation.

Update to OWL API 3.5.3

Using the generic algorithm to generate (logical) explanations for why is owl:Nothing a subclass of a class expression in the DL Query tab starts an infinite process that the user will need to interrupt in order to regain control, and returns a long list of results that are very difficult to interpret.

I would suggest that we treat owl:Nothing as a special case, and generate a "smarter", i.e. a more meaningful, explanation for why is owl:Nothing listed among the subclasses of any given class expression (e.g. "because owl:Nothing is the bottom class (and it is equal to the empty set) and therefore it is subclass of every class").

If you have previously displayed explanations for an inference in Protege, and then request explanations for a different inference, the progress panel will display the number of explanations found in the previous usage when it is first displayed. For example, if on the first run it says "Computing explanations. Found 1", then the next time you use it, it immediately starts with "1". So there is no way to know when it finds the first one (I usually wait until it gets to 2 so that something changes).

The progress dialog has a fake parent that is not the workspace frame. This can sometimes cause the UI to freeze (or at least appear to freeze).

It is confusing that the justification for an entailment that was asserted in the ontology shows an empty box.

Currently the axioms that are part of a justification cannot be copied to the clipboard, or exported in any other way. This may be a useful feature.

It seems that if the axiom is a tautology (is entailed from the empty set of axioms), incorrect explanations are produced.

To reproduce:

1. open any ontology, e.g., Pizza
2. go to DL Query tab and enter some conjunction, e.g., American and Pizza
3. compute the superclasses of the query
4. press explain (?) next to the conjunct appearing in the query, e.g., "Pizza"

Expected result:
only the empty explanation should be shown

Actual result:
the computation does not seem to terminate; if interrupted it shows many explanations with one axiom from the ontology but also with some axioms like <Entailmentxxxxx> SubClassOf ...

SubPropertyOf axioms have a colon, but not SubClassOf.

If two classes are inferred by ELK to be equivalent due to being reciprocal subclasses, trying to get an explanation will result in a blank window. This does work with HermiT. You must try with ELK before trying with HermiT, because if HermiT has already provided an explanation, it will simply be shown again when you repeat with ELK. Here is an example ontology:

Prefix(:=<http://example.org/>)
Prefix(owl:=<http://www.w3.org/2002/07/owl#>)
Prefix(rdf:=<http://www.w3.org/1999/02/22-rdf-syntax-ns#>)
Prefix(xml:=<http://www.w3.org/XML/1998/namespace>)
Prefix(xsd:=<http://www.w3.org/2001/XMLSchema#>)
Prefix(rdfs:=<http://www.w3.org/2000/01/rdf-schema#>)

Ontology(<http://example.org/>

Declaration(Class(<http://example.org/#A>))
Declaration(Class(<http://example.org/#B>))
Declaration(Class(<http://example.org/#C>))
Declaration(Class(<http://example.org/#D>))

EquivalentClasses(<http://example.org/#A> <http://example.org/#D>)

EquivalentClasses(<http://example.org/#B> <http://example.org/#C>)

SubClassOf(<http://example.org/#B> <http://example.org/#A>)

SubClassOf(<http://example.org/#D> <http://example.org/#C>)

)

Run the reasoner, select term A, then get explanation for equivalence with B.

@matthewhorridge this is the issue I mentioned.

See protegeproject/protege#410

The tooltip that appears when hovering over different axioms that are part of an explanation shows "Inferred", which is inaccurate. I am not sure what the is the exact intent of these tooltips, but, these axioms are asserted, not inferred.

The current version is 3.3.0 which causes some problems. See protegeproject/protege#100

Level: INFO
Time: 1490807563311
Message: [Explanation] Computing justifications for EquivalentObjectProperties(http://www.semanticweb.org/rgoncalves/ontologies/2017/2/untitled-ontology-1075#absorbs owl:bottomObjectProperty )
Level: INFO
Time: 1490807563382
Message: [Explanation] A total of 0 explanations have been computed