Issue Tracker & Infinite Loop Bug

[Daniel Smullen]

Hello HermiT team,

I'm a PhD student at Carnegie Mellon University, at the Institute for Software Research. I am working on a project that leverages HermiT for reasoning over potentially large ontologies. In exploration of the scalability to that end, I have discovered what I am certain is a bug, in reasoning about satisfiability over a consistent (at least, reported by the API as such) ontology.

As of this past August, Google Code has made the HermiT project read-only, and therefore no new issues can be reported using that method. It seems that this is the only supported issue tracker as prescribed by the HermiT official webpage. Is there an alternative being cooked up? Where can I report issues, other than here in the forums? Is there someone in charge of the project at Oxford or somewhere else who we can reasonably expect to hear back from if we email them?

Anyway, I've been able to reproduce the bug consistently on the attached ontology, which appears to be consistent when invoking the consistency checks using the Java API. However, when I try to return the flattened ontology, it loops forever. Debugging, I see that it is trying to determine the satisfiability of something in the ontology, but failing. What's more, I can open this ontology in Protege and see that it's fine, save for some kind of inconsistency related to the Nothing concept. When I try to query for an explanation, the same looping behavior occurs. See the attached OWL file.

Is there any explanation for this odd behavior that I may have overlooked? Why does it occur every time I attempt to get the flattened ontology?

[Ignazio Palmisano]

On 20 October 2015 at 23:20, Daniel Smullen

<biggest.no...@gmail.com> wrote:
> Hello HermiT team,
>
> I'm a PhD student at Carnegie Mellon University, at the Institute for
> Software Research. I am working on a project that leverages HermiT for
> reasoning over potentially large ontologies. In exploration of the
> scalability to that end, I have discovered what I am certain is a bug, in
> reasoning about satisfiability over a consistent (at least, reported by the
> API as such) ontology.

I've tried replicating your issue on HermiT 1.3.8.5-SNAPSHOT (the
version that uses OWLAPI 4.0.2) and I could not replicate it - I've
tested satisfiability of all the classes in the ontology signature and
it completed within seconds.

HermiT 1.3.8.5-SNAPSHOT is available here:


https://github.com/ignazio1977/ore2015submission

The code I've used:

import org.semanticweb.HermiT.Reasoner;
import org.semanticweb.owlapi.apibinding.OWLManager;
import org.semanticweb.owlapi.model.OWLClass;
import org.semanticweb.owlapi.model.OWLOntology;
import org.semanticweb.owlapi.model.OWLOntologyCreationException;
import org.semanticweb.owlapi.profiles.Profiles;
import org.semanticweb.owlapi.reasoner.OWLReasoner;

public class TestBadOntology {

public static void main(String[] args) throws OWLOntologyCreationException {
OWLOntology o =
OWLManager.createOWLOntologyManager().loadOntologyFromOntologyDocument(TestBadOntology.class
.getResourceAsStream("/example.conflicts.bad.owl"));
System.out.println("TestBadOntology.main() " +
Profiles.OWL2_DL.checkOntology(o));
OWLReasoner r = new Reasoner.ReasonerFactory().createReasoner(o);
System.out.println("TestBadOntology.main() " + r.isConsistent());
System.out.println("TestBadOntology.main() " +
r.getUnsatisfiableClasses());
for (OWLClass c : o.getClassesInSignature()) {
System.out.println("TestBadOntology.main() " +
r.getSubClasses(c, false).getFlattened());
}
}
}

As far as I'm aware, this version of HermiT should not have any
performance differences or significant bugs with respect to the main
HermiT release - it just uses a newer OWLAPI version.

It might be that the difference is in the class expression you're
passing in - if this doesn't work for you, can you show what value
you're passing for c?

Cheers,
Ignazio

>
> As of this past August, Google Code has made the HermiT project read-only,
> and therefore no new issues can be reported using that method. It seems that
> this is the only supported issue tracker as prescribed by the HermiT
> official webpage. Is there an alternative being cooked up? Where can I
> report issues, other than here in the forums? Is there someone in charge of
> the project at Oxford or somewhere else who we can reasonably expect to hear
> back from if we email them?
>
> Anyway, I've been able to reproduce the bug consistently on the attached
> ontology, which appears to be consistent when invoking the consistency
> checks using the Java API. However, when I try to return the flattened
> ontology, it loops forever. Debugging, I see that it is trying to determine
> the satisfiability of something in the ontology, but failing. What's more, I
> can open this ontology in Protege and see that it's fine, save for some kind
> of inconsistency related to the Nothing concept. When I try to query for an
> explanation, the same looping behavior occurs. See the attached OWL file.
>
> Is there any explanation for this odd behavior that I may have overlooked?
> Why does it occur every time I attempt to get the flattened ontology?
>

> --
> You received this message because you are subscribed to the Google Groups
> "HermiT Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to hermit-users...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.