ElkReasoner VersionInfo breaks for -SNAPSHOT versions. Also, get top/bottom data/object property node methods not implemented

[GoogleCodeExporter]

This patch: 
   1)  Ignores  trailing non digits in a version number components. 
   2) Returns nodes containing all the properties which ELK indicates are equivalent to owl:topObjectProperty etc.  (i.e. just return the constants from org.semanticweb.owlapi.reasoner.impl.OWLObjectPropertyNode ).

Also, I may be wrong, but it  the case for EL that if one generates named 
equivalent classes for any complex class expressions used in a DisjointClasses 
Axiom, one can find the disjoint classes for an expression CE by finding all 
the DisjointClasses axioms where one of the disjoints is a super class of CE, 
and combining the subclasses of the other disjoints?  

It's sound and fast, but I'm not sure if naming the disjoints  is enough for 
completeness?

Original issue reported on code.google.com by [email protected] on 4 Mar 2015 at 2:45

Attachments:

• ElkReasoner.patch

[GoogleCodeExporter]

Hi, thanks for the patch!

Can you comment what was the problem fixed by the change 1)?

Regarding your changes to the methods for getBottomObjectPropertyNode()  etc., 
how do you make sure that the equivalent properties and super-properties are 
reported by ELK? I can see the calls to the methods like 
OWLObjectPropertyNode.getBottomNode(), which do not seem to involve ELK at all. 
This would be very surprising given that ELK does not currently implement 
checking equivalences an inclusions of object and data properties.

Regarding your suggestion for checking disjoint classes, the problem is that 
disjointness can be stated not only by DisjointClasses axioms but can be 
consequence of other axioms, e.g., SubClassOf(ObjectIntersectionOf(:C1 :C2) 
owl:Nothing)), or even more complex situations. I agree that your test is sound 
and be implemented fast, but it is incomplete.

Original comment by [email protected] on 4 Mar 2015 at 2:18

[GoogleCodeExporter]

The problem fixed by change 1 was that the getting the reasoner version would 
throw a NumberFormatException. (I am using reasoner version to record inference 
provenance.   The real bug is in the OWLAPI definition of VersionInfo, which 
ought to do its own parsing. 

Re: top/bottom property nodes : 
    There does not exist any property P such that ELK indicates it is equivalent to the top (bottom) property and it is not added to the returned node. :)   Hence the faux :)
  The main purpose is to stop protege from throwing an exception in a place where it shouldn't even be calling the reasoner at all (without changing settings when switching between reasoners). 

more thoughts on  disjoints: 

The form  "SubClassOf(ObjectIntersectionOf(:C1 :C2) owl:Nothing))" is an EL 
legal syntactic transform of DisjointClasses (I think the other usual forms 
require the use of negation).  

 If all complex class expressions are named, any unsatisfiable class that is equivalent to an intersection may be a "hidden disjoint classes".

If any of the conjuncts are unsatisfiable,  testing must be done on the 
remaining conjuncts.

If there are precisely two conjuncts, and both of them are not unsatisfiable, 
then a disjoint classes expression has been found. 

If more than two conjuncts are present, and none of them are unsatisfiable, 
then the elements must be tested for pairwise disjointness. 
 If any combinations of conjuncts, less than the whole, is a superclass of some satisfiable named class, then the remaining conjuncts  (and named combinations) must be tested for pairwise disjointness with that class.     
This part is potentially scary,but because it is restricted to  combinations 
that were named before classification it should be less so.  

If all complex class expressions are named, are there any EL cases other than 
unsatisfiable intersectionOf's that entail disjoint named classes?  Conversely, 
if there are no unsatisfiable classes, are explicit DisjointClasses axioms the 
only source of disjointness?

Original comment by [email protected] on 4 Mar 2015 at 8:51