search

ha-mo-we / Racer

Racer is a knowledge representation system that implements a highly optimized tableau calculus for the description logic SRIQ(D).
Other
106 stars 19 forks source link

Surprizing test case showing magical reasoning capability ... #18

Closed gschadow closed 5 years ago

gschadow commented 5 years ago

Here is the simplest test case for something that RACER does, that I want, but I have no idea why I am able to get this result. I don't know how else I could get this result,. But I don't know why I am getting it. Full case here:

(delete-all-tboxes)

(equivalent Part-bearer
  (some has-part (not Part-bearer)))

(range has-part (not Part-bearer))
(implies-role has-stuff has-part)

(implies X Y)
(equivalent Z
  (some has-part
    (some has-part
      (some has-part
        (some has-stuff X)))))

(concept-subsumes? (some has-stuff X) Z)
(concept-subsumes? (some has-stuff Y) Z)
(check-tbox-coherence)

Turns out that the role has-stuff is transferred through has-part as if that role was defined as a composition with the transitive has-part role. But this feature doesn't even exist in RACER (though I really need it ... and it looks like I found a way to emulate it?)

The concept Z is not satisfiable because of the range constraint (not Part-bearer). But when I remove that constraint, then the has-stuff role no longer transfers through the has-part role.

ha-mo-we commented 5 years ago

Given that z is not satisfiable, i.e., empty, it is clear that (concept-subsumes? (some has-stuff X) Z) and (concept-subsumes? (some has-stuff Y) Z) return t.

Now, what makes z unsatisfiable given that (range has-part (not Part-bearer)) is included? For each z there exists a filler of has-part, which, due to the range declaration, is an instance of (not part-bearer). For the filler of has-part of a z instance, in turn, there exists a has-part filler of type (not part-bearer), again due to the has-part range declaration. But, (not part-bearer) for the first filler indeed implies (all has-part (not (not part-bearer))) is true for the second due to (equivalent part-bearer (some has-part (not part-bearer))), and therefore for the second filler in the chain mentioned above we have a clash. Thus, there cannot be an instance of z.

Hope this helps. Thank you for your interest in Racer.

Best regards, Ralf

Univ.-Prof. Dr. rer. nat. habil. Ralf Möller Direktor

UNIVERSITÄT ZU LÜBECK INSTITUT FÜR INFORMATIONSSYSTEME

Ratzeburger Allee 160
23562 Lübeck

Phone: +49 451 3101 5700
Cellphone: +49 176 5694 6432
Email: moeller@uni-luebeck.de
Web: http://www.ifis.uni-luebeck.de/~moeller
gschadow commented 5 years ago

Thanks for your reply, and consider the whole thing moot. I understand that it isn't satifisfiable, and since you already implemented role composition, this is only a curiosity of no further relevance. I am delighted you are still here taking care of things. Thank you!