Wednesday 7 November 2012

Inconsistent and unsatisfiable?

I am currently developing an ontology that described the process of generalisation to facilitate on-demand mapping.  This has not been an easy process. I think the mental processes required when designing an ontology is totally different from that required when designing a relation database, say.

Anyway, I had been confused by the meaning of an inconsistent ontology and a unsatisfiable class. This can be seen by creating (in Protégé 4.2) a class, Material.  Under this class create two disjoint Subclasses Chalk and Cheese. They will have the same definition.  Make the Cheese class a defined class.  Run a reasoner. The Chalk class will be flagged (in red) as unsatisfiable - it cannot contain any individuals.  In this case it is because both classes are disjoint but have the same definition; by definition any individual created in Chalk will be in the (defined) Cheese class but it cannot because they are disjoint.  If you now create an individual in Chalk and synchronize the reasoner, the whole ontology is now inconsistent. This can be tested using the OWL API (3.2) by using the OWLReasoner methods getUnsatisfiableClasses and isConsistent.

An individual created in an unsatisfiable class is not the only reason an ontology becomes inconsistent. It might occur when the Functional characteristic of a property is violated.