Let's say that we have an ontology like the following:

  1. A ≡ B ⊓ C
  2. A ≡ D ⊔ F
  3. G ≡ C ⊓ A

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:

A ≡ (B ⊓ C) ⊓ (D ⊔ F)

or is this totally wrong?

In a few words:

How does a reasoner handle multiple class definitions?

asked 11 Jul '12, 05:02

Kostas's gravatar image

Kostas
15717
accept rate: 0%

edited 11 Jul '12, 10:03

There is something wrong in your expression A ≡ (B ⊓ C) ⊓ (A ≡ D ⊔ F). There cannot be the symbol twice in a DL formula.

(11 Jul '12, 09:51) Antoine Zimm... ♦ Antoine%20Zimmermann's gravatar image

Fixed. copy-paste error :)

(11 Jul '12, 10:06) Kostas Kostas's gravatar image

I guess the next question would be which reasoner? :) As per Antoine's answer, a reasoner may not use unfolding at all.

Aside from this, your new definition for A is correct, since B ⊓ C ≡ D ⊔ F ... and intersecting two equivalent classes "does nothing". Seems a bit pointless though. :)

By the way, G ≡ A.

(11 Jul '12, 11:59) Signified ♦ Signified's gravatar image

No. My only question is how a reasoner handles these cases:) I know that most reasoners use tableau algorithms. So, when the algorithm meets a branch like A, how does it expand it? Does it create a new branch for each definition of A?

G ≡ A: Now everything makes sense :P

(11 Jul '12, 12:22) Kostas Kostas's gravatar image

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 A at all.

permanent link

answered 11 Jul '12, 06:52

Antoine%20Zimmermann's gravatar image

Antoine Zimm... ♦
10.2k514
accept rate: 32%

Yes, I know that Protege is not a reasoner. I meant that when I call a reasoner (through Protege), it can handle multiple equivalent classes.

What I want to know is how a reasoner handles such cases. My initial question was not very clear. I edited it :)

(11 Jul '12, 07:05) Kostas Kostas's gravatar image

Let's assume you want to check the consistency of your ontology. One way to do it is to verify that the concept:

(¬A ⊔ (B ⊓ C)) ⊓ (A ⊔ ¬(B ⊓ C)) ⊓ (¬A ⊔ (D ⊔ F)) ⊓ (A ⊔ ¬(D ⊔ F)) ⊓ (¬G ⊔ (C ⊓ A)) ⊓ (G ⊔ ¬(C ⊓ A))

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.

permanent link

answered 01 Aug '12, 06:04

Antoine%20Zimmermann's gravatar image

Antoine Zimm... ♦
10.2k514
accept rate: 32%

But in some point in the tableuax algorithm process, we need to expand the A (or ¬A) concept. Don't we?

Or because we have already encoded the information that the A concept is subclass and superclass of the others (in the concept you defined), there is no need for a further expansion?

(01 Aug '12, 06:26) Kostas Kostas's gravatar image

No, you don't need to expand anything. The algorithm does not even need to know what the original axioms are, it simply needs the concept I mentioned as input.

(02 Aug '12, 02:39) Antoine Zimm... ♦ Antoine%20Zimmermann's gravatar image
Your answer
toggle preview

Follow this question

By Email:

Once you sign in you will be able to subscribe for any updates here

By RSS:

Answers

Answers and Comments

Markdown Basics

  • *italic* or _italic_
  • **bold** or __bold__
  • link:[text](http://url.com/ "title")
  • image?![alt text](/path/img.jpg "title")
  • numbered list: 1. Foo 2. Bar
  • to add a line break simply add two spaces to where you would like the new line to be.
  • basic HTML tags are also supported

Question tags:

×66
×8

question asked: 11 Jul '12, 05:02

question was seen: 1,058 times

last updated: 31 Oct '12, 10:16