Wednesday, February 28, 2007

DL riddle

Yesterday we stumbled upon quite a hard description logics problem. At least I think it is hard. The question was, why is this ontology unsatisfiable? Just six axioms. The ontology is availbe in OWL RDF/XML, in PDF (created with the owl tools), and here in Abstract Syntax.

Class(Rigid complete restriction(subclassof allValuesFrom(complementOf(AntiRigid))))
Class(NonRigid partial)
DisjointClasses(NonRigid Rigid)
ObjectProperty(subclassof Transitive)
Individual(publishedMaterial type(NonRigid))
Individual(issue type(Rigid) value(subclassof publishedMaterial))

So, the question is, why is this ontology unsatisfiable? It is even a minimally unsatisfiable subset, actually, that means, remove any of the axioms and you get a satisfiable ontology. Maybe you like to use it to test your students. Or yourself. The debugger in SWOOP actually gave me the right hint, but it didn't offer the full explanation. I figured it out, after a few minutes of hard thinking (so, now you know how bad I am at DL).

Do you know? (I'll post the answer in the comments if no one else does in a few days)

(Just in case you wonder, this ontology is based on a the OntOWLClean ontology from Chris Welty, see his paper at FOIS2006 if you like more info)


Blogger denny said...

The problem is that subclassof is transitive, thus every Rigid's class subclass must be Antirigid -- and also their own subclasses, etc. due to transitivity. But this actually makes every subclasof a rigid class rigid as well, because all of its subclasses will be antirig! And so, PublishedMaterial becomes rigid. But this is not possible, because it is declared non-rigid explicitly.

Wow. I found that hard.

March 13, 2007 12:18 AM  
Anonymous Copy Paste Your Name said...

Gasp! I thought I put a comment on this. Did I?

September 14, 2007 11:21 AM  
Anonymous As stoopid as a penis said...

I make a very subversive intrusion into this web log by giving an interpretation of your so called "unsatisfiable ontology".
Consider the domain of interpretation D = {a,b}. Consider the function of interpretation I such that:

I(issue) = a
I(publishedMaterial) = b
I(Rigid) = {a}
I(NonRigid) = {b}
I(AntiRigid) = {} (i.e., empty set)
I(subclassof) = {(a,b)}

This is a model of the ontology. Proof: it satisfies all the axioms of the ontology. Indeed:
1) I satisfies NonRigid(publishedMaterial) because I(publishedMaterial) is in I(NonRigid);
2) I |= Rigid(Issue) because I(issue) is in I(Rigid);
3) I |= subclassof(issue,publishedMaterial) because the pair (I(issue),I(publishedMaterial)) is in I(subclassof);
4) I |= disjunct(NonRigid,Rigid) because no elements of I(NonRigid) is in I(Rigid) and vice versa;
5) I |= equivalent(Rigid,forall(subclassof,not( AntiRigid)) because the only element of I(Rigid), namely a, is in relation with an element that is not in I(AntiRigid) via relation I(subclassof). Moreover, it is the only entity involved in such relation. So there is an equivalence.
6) I |= Trans(subclassof). Indeed, I(subclassof) is trivially transitive.

Now, you say that SWOOP can prove it unsatisfiable. Therefore, either SWOOP does not implement a correct reasoner, or my interpretation is not a model of the ontology (in which case, my proof is not a proof).

September 14, 2007 12:27 PM  

Post a Comment

Links to this post:

Create a Link

<< Home