Argh, its all turned red again
Most reasoners do not provide any explanation as to why classes are unsatisfiable. It is therefore down to people to trace down the cause of their inconsistencies by hand, which is non-trivial because:
- Inferences can be indirect and non-local. Axioms can have wide-ranging effects which are hard to predict.
- Unsatisfiability propagates. Therefore, a single root error can cause many classes to be marked as unsatisfiable. Identifying the root error from amongst the mass of unsatisfiable classes is difficult.
Several groups, including the HyOneUse/CO-ODE project (see our paper), are trying to build tools to help people debug OWL-DL ontologies. Currently the preliminary version of our debugger has been build and being tested. Other tools are also at this stage, and it would be useful to have a series of test ontologies to try to break them.
If you have any difficulties figuring out the reason your classes are inconsistent, please send the ontologies to us.
With your permission, we'd like to publish them so that other groups can use them as test-data.
In return, you never know, we might be able to help email@example.com