Let's say that we have an ontology like the following:
If a reasoner tries to unfold the G concept, which concept will replace A? The (B ⊓ C) or the (D ⊔ F)?
In The Description Logic Handbook it says that a TBox can be unfolded only if all its axioms are unique and acyclic definitions. However, in Protege, I can define a class that is equivalent to more than one other classes, and the reasoning process works fine. How does a reasoner handle these cases? Would it be possible to redefine concept A as:
or is this totally wrong?
In a few words:
How does a reasoner handle multiple class definitions?
A reasoner can handle this in many different ways and does not need to use unfolding at all. In any case, Protégé is not a reasoner and it can be used to edit ontologies that OWL DL reasoners cannot even handle. However, it is possible to use a reasoner inside Protégé because Protégé is pluggable. By default, Protégé includes at least a reasoner (which depends on the version you use).
In any case, multiple equivalent classes are not a problem with current reasoners and you don't have to redefine concept
answered 11 Jul '12, 06:52
Antoine Zimm... ♦
Let's assume you want to check the consistency of your ontology. One way to do it is to verify that the concept:
is satisfiable, which means that there can be an instance of this concept without inconsistency. Put this in conjunctive normal form, apply standard tableaux algorithms, and you're done. This is one way to do it, there are others. For instance, the ontology you define with these three axioms only contains boolean constructs and no negation. A reasoner can simply answer "yes" to a consistency check without any formal manipulation. You could also apply rule-based resolution which would lead to the same conclusion.
answered 01 Aug '12, 06:04
Antoine Zimm... ♦