Ontologies are sets of semantic constraints describing application domains; when constraints change, they may become inconsistent. To restore consistency, the whole set of constraints must be changed again, but this may destroy the original ontology.

This paper describes a method to avoid this danger. It starts from existing knowledge representation languages, called description logics, focusing on SHIQ in particular, and from tableau algorithms, which are procedures to prove or disprove assertions expressed in such languages. Tableau algorithms are presently used to build forests, or sets of ontologies describing the same knowledge domain with different semantics. The problem when using tableau algorithms, however, is that they can lead to sets with an explosive number of ontologies, often in conflict with each other.

The advancement this paper proposes to the field is a method to prevent building infinite sets of ontologies when using tableau algorithms and stopping instead as soon as inconsistencies arise among them; the paper calls this the least path. This method is described first in general terms, and then in an optimized way in order to find the least path as before, but with the fewest steps possible. The paper at first makes extensive use of formal logic notation to describe the method; the extensive use in this context of tables and graphs to summarize logic rules is a great help. Then, to test the method on live data, an algorithm written in pseudocode is introduced and run on three real ontologies; results are then evaluated and compared, again in table form. A final section highlights the weaknesses of the model to be addressed and eliminated in future work.

Although the paper is not easy reading, because only an in-depth knowledge of formal logic will allow the reader to appreciate its subtleties, it presents detailed and innovative contributions to the field and would certainly be recommended reading for those familiar with formal logic.