ELK and Hermit do not agree on satifability

[Nacho Traverso Ribón]

Hello everyone,

I am working with the gene ontology and I want to move from HermiT to ELK since I am using only EL axioms. I am trying to check the entailment of a subclassOf axiom of the type A SubClassOf (p some B). To do that I am checking the satisfability of the axiom A and NOT(p some B). If the call isSatisfiable(A and NOT(p some B)) returns false, that means that A is necessarily subsumed by the class expression p some B. Hermit is able to answer correctly to this query. However, ELK returns always true. I have compared the results of HermiT and ELK for the same axiom and the results differs. What I am doing wrong? Which is causing the difference of results?

Thank you in advance
Ignacio Traverso

[Yevgeny Kazakov]

Dear Ignacio,

This should, in principle, work. I assume that you call the reasoners
though OWL API. Can you provide a small example that can be tested?
Best, if you could create a ticket and put all details there:

https://code.google.com/p/elk-reasoner/issues/list

Just to double check, if instead of checking satisfiability of

A and NOT(p some B)

you add an axiom

X SubClassOf (A and NOT(p some B))

where X is some new class, and then check satisfiability of X. Do you
obtain the right result?
Because this is what ELK should be doing under the hood when this
method is called.

Best regards,

Yevgeny

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

[Yevgeny Kazakov]

Hi, I just made a quick test with the pizza ontology [1] and ELK v.0.4.2 and everything seems to work as expected.
Here is a code, which is a minor modification of [2]:

public class QueryingClassSatisfiability {

public static void main(String[] args) throws OWLOntologyCreationException {

OWLOntologyManager man = OWLManager.createOWLOntologyManager();

OWLDataFactory dataFactory = man.getOWLDataFactory();

// Load your ontology.

OWLOntology ont = man.loadOntologyFromOntologyDocument(new File(

"/path/to/pizza.owl"));

// Create an ELK reasoner.

OWLReasonerFactory reasonerFactory = new ElkReasonerFactory();

OWLReasoner reasoner = reasonerFactory.createReasoner(ont);

// Create your desired query class expression. In this example we

// will query ObjectIntersectionOf(A ObjectComplementOf(ObjectSomeValuesFrom(R B))).

PrefixManager pm = new DefaultPrefixManager(

"http://www.co-ode.org/ontologies/pizza/pizza.owl#");

OWLClass A = dataFactory.getOWLClass(":American", pm);

OWLObjectProperty R = dataFactory.getOWLObjectProperty(":hasTopping",

pm);

OWLClass B = dataFactory.getOWLClass(":MeatTopping", pm);

OWLClassExpression query = dataFactory.getOWLObjectIntersectionOf(A,

dataFactory.getOWLObjectComplementOf(dataFactory

.getOWLObjectSomeValuesFrom(R, B)));

System.out.println("isSatisfiable(" + query + ") = "

+ reasoner.isSatisfiable(query));

reasoner.dispose();

}

}

Here is the output:

isSatisfiable(ObjectIntersectionOf(<http://www.co-ode.org/ontologies/pizza/pizza.owl#American> ObjectComplementOf(ObjectSomeValuesFrom(<http://www.co-ode.org/ontologies/pizza/pizza.owl#hasTopping> <http://www.co-ode.org/ontologies/pizza/pizza.owl#MeatTopping>)))) = false

If I change

OWLClass A = dataFactory.getOWLClass(":American", pm);

to

OWLClass A = dataFactory.getOWLClass(":Margherita", pm);

the output is:

isSatisfiable(ObjectIntersectionOf(<http://www.co-ode.org/ontologies/pizza/pizza.owl#Margherita> ObjectComplementOf(ObjectSomeValuesFrom(<http://www.co-ode.org/ontologies/pizza/pizza.owl#hasTopping> <http://www.co-ode.org/ontologies/pizza/pizza.owl#MeatTopping>)))) = true

as expected.

Can you test this code if it works for you?

Best regards,

Yevgeny

[1] http://protege.stanford.edu/ontologies/pizza/pizza.owl
[2] https://code.google.com/p/elk-reasoner/wiki/QueryingComplexClasses

[Nacho Traverso Ribón]

Hi,

you are right. The code you provided is working. To get the complement of a class I was using the function getComplementNNF() of OWLClassExpression. Now, I changed to factory.getOWLObjectComplementOf() and it is working.

Thank you for your help
Ignacio Traverso