ISWC08 Monday p.m.

I've had lunch and coffee and I'm ready for more. This afternoon promises the most relevant sessions so far. Will I sink or swim?

"Moduralisation and Explanation" a.k.a. "Understanding and repairing inferences"
Matthew Horridge & Uli Sattler

There's a customised version of Protege 4 that's used in this session available at the tutorial web site, and a couple of example ontologies to go with it. Specifically, the customised Protege 4 comes with some plug-ins that are part of the TONES project.

Uli starts by leading us in gently. There are lots of ontologies out there & if one contains concepts that you want to model you should reuse them. This is sound engineering technique & makes perfect sense. However, you might want to reuse only a part of an ontology, so how do you go about extracting the useful bit? Well, you can probably identify the concepts that you want to reuse, but they themselves will depend on other concepts within the borrowed ontology & you'll need to import those borrowed concepts as well, and this is called 'coverage'. The bad news is that guaranteeing coverage is, in general, undecidable, but there is a syntactic approximation (phew) that guarantees coverage, but not minimal size.

Unfortunately (again) you can't guarantee the 'safety' of the imported terms. There may be clashes or inconsistencies with your ontology and you'll need to check these manually. This is related to "Conservative extensions" (what ever they may be) and is the subject of ongoing research.

Now Matthew takes over, and we get into some gritty inference stuff. Using a reasoner plugin he identifies a number of Root & Derived Unsatisfiable classes in the ontology. These are generally 'Bad Things' (TM) - after all what's the point of a class that nothing CAN belong to (note this is different from an empty class, that is satisfiable, but has no members). The plugin lists the unsatisfiable classes, and shows which are Root classes - these need to be addressed first, because fixing them might well fix the unsatisfiability of the Derived classes.

In a large ontology (or any ontology) it can be hard for a mere human to determine _why_ a class is unsatisfiable. Lucky for us, reasoners can be induced to tell us. What they can give us is 'justifications' which are "minimal subsets of an ontology that are sufficient for a given entailment (inference) to hold". They are a sort of explanation of how an inference was reached (and are also known as MUPS or MinAs). Each justification is made up of one or more axiom, and the same axiom may occur in more than one justification. For a given inference (such as the unsatisfiability of a class) there may be multiple justifications. To 'repair' an unsatisfiability all you need to do is delete a single axiom from each if the justifications. Of course, nothing is that simple - how do you know which axiom (s) to delete? Well, you need to analyse the axioms and decide which ones represesent logical errors.

So far, so good. Now things begin to get a bit hairy.

Some justifications include 'superfluous' axioms - the same inference would ave been reached if those axioms didn't exist. This might point to problems in the ontology, and there's a plugin to help find these. The superfluous nature of these justifications can be concealed by both 'Internal' and 'External' masking, which I'm not even going to try and explain. Then there are 'Fine-grained' justifications that come in two flavours: 'Laconic' and 'Precise'. The plug-in lets you look at the 'Laconic', which have no superfluous axioms, and all axioms are as weak as possible. 'Precise' justifications are a subset of 'Laconic' justifications and are primarily geared towards repair.

Well, I'm glad that's all clear.


"Data Integration through Ontologies"
Diego Calvanese & Giuseppe De Giacomo

Still to come....