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

A strange case ... #21

Open gschadow opened 5 years ago

gschadow commented 5 years ago

Sorry to bother with lots of issues. I'm developing a really serious ontology and there is complexity here. So I get some strange cases. This here I have boiled down as much as I could. Cut and paste the rest here (I have text commented out to make it really easy). It starts with setting up the RBox and TBox, then a simple subsumption test, then I add one more axiom, that seems to have nothing to do with the test, but that changes the test result.

Concepts: A, B, C, D Roles: R, S, T, U, V

(delete-all-tboxes)

; BEGINNING OF CASE

(implies A (some R B))
(domain R A)
(implies-role (S R) R)
(transitive S)
(implies-role (T V U) T)

; now here is a test

(concept-subsumes? A (some S (some R B))) ; => T good!

; now we add one more axiom

(implies (some T D) (some S C))

; and test again

(concept-subsumes? A (some S (some R B))) ; => NIL bad!

; but strangely, if I test with the definition of A instead of atom A, it works:

(concept-subsumes-p (get-concept-definition A) '(some S (some R B)) 'default) ; => T

; END OF CASE

Sorry I couldn't figure out a way to make the test case any simpler than this. Every line is necessary, and even the role V that is never used anywhere else.

I'd appreciate your thoughts.

regards, -Gunther

gschadow commented 5 years ago

Could it be that I don't fully understand the significance of domain axioms? If I change 

(implies A (some R B))
(domain R A)

to

(equivalent A (some R *TOP*))

then my problem resolves.

But why is that?

gschadow commented 5 years ago

Update: I have decided to stay away from using any domain and range axioms. The reason is that they "force" a concept assumption on the bearer or value of a role, which might actually be an error. When I removed domain and range axioms on my work in progress, I found many problems that ultimately were errors in my axioms.

ha-mo-we commented 5 years ago

On 17. Jul 2019, at 18:55, gschadow notifications@github.com wrote:

Update: I have decided to stay away from using any domain and range axioms.

(domain r c) is an abbreviation for (implies (some r top) c) (range r c) is an abbreviation for (implies (some (inv r) top) c)

For range restrictions, the inverse of r can be handled in a special way such that the tableau calculus for inverse roles is not activated. This calculus in much less efficient in general.

-Ralf

The reason is that they "force" a concept assumption on the bearer or value of a role, which might actually be an error. When I removed domain and range axioms on my work in progress, I found many problems that ultimately were errors in my axioms.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ha-mo-we/Racer/issues/21?email_source=notifications&email_token=AB2476WD35M5WIT5H7VTPXDP75FI7A5CNFSM4ICVI7FKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD2FBFZA#issuecomment-512365284, or mute the thread https://github.com/notifications/unsubscribe-auth/AB2476V4VZTNBBVJYJAH6NLP75FI7ANCNFSM4ICVI7FA.

gschadow commented 5 years ago

(range r c) is an abbreviation for (implies (some (inv r) top) c)

Does anyone have a recommended reading that explains how I can use the role inverse in TBox reasoning? It strikes me that one can never deduce from (equivalent C1 (some R C2)) that (implies C2 (some (inv R) C1)). And that (range R C) doesn't seem to have an effect on the concept C outside of the scope of the current role restriction on R, does it?

It seems to me that inverse roles really only work when constructing ABox instances, where then specific role instances can match a pair of mutually inverse roles in the TBox definitions. But I see no way how to relate two role restrictions with inverse roles in any way.

I have a case, for example. Two concepts which are related by inverse roles:

(equivalent Powder-for-solution-for-injection
  (and Powder
     (some is-input-of 
         (and Dissolution-process
             (some has-product Solution-for-injection-from-powder)))))

and 

(equivalent Solution-for-injection-from-powder
  (and Solution-for-injection
    (some is-product-of
       (and Dissolution-process
          (some has-input Powder-for-solution-for-injection)))))

with

(define-primitive-role has-product :inverse is-product-of)
(define-primitive-role has-input :inverse is-input-of)

All I could do with this so far was to chase RACER into an infinite cycle. But I don't know how I might relate the two concepts to find out that they are actually the same thing viewed from two different angles.

ha-mo-we commented 5 years ago

Please try

(in-package :racer-user)

(in-knowledge-base test)

(define-primitive-role is-product-of :inverse has-product)

(define-primitive-role is-input-of :inverse has-input)

;;(inverse has-product is-product-of) should work doesn't (is-product-of unknonwn role) ;;(inverse has-input is-input-of) ditto

(equivalent Powder-for-solution-for-injection (and Powder (some is-input-of (and Solution-process (some has-product Solution-for-injection-from-powder)))))

(equivalent Solution-for-injection-from-powder (and Solution-for-injection (some is-product-of (and Solution-process (some has-input Powder-for-solution-for-injection)))))

(check-tbox-coherence) ; ---> (nil nil) no unsatisfiable concepts, no unsatisifiable roles

-Ralf

On 19. Jul 2019, at 03:37, gschadow notifications@github.com wrote:

(range r c) is an abbreviation for (implies (some (inv r) top) c)

Does anyone have a recommended reading that explains how I can use the role inverse in TBox reasoning? It strikes me that one can never deduce from (equivalent C1 (some R C2))' that (implies C2 (some (inv R) C1))`. And that (range R C) doesn't seem to have an effect on the concept C outside of the scope of the current role restriction on R, does it?

It seems to me that inverse roles really only work when constructing ABox instances, where then specific role instances can match a pair of mutually inverse roles in the TBox definitions. But I see no way how to relate two role restrictions with inverse roles in any way.

I have a case, for example. Two concepts which are related by inverse roles:

(equivalent Powder-for-solution-for-injection (and Powder (some is-input-of (and Solution-process (some has-product Solution-for-injection-from-powder))))) and

(equivalent Solution-for-injection-from-powder (and Solution-for-injection (some is-product-of (and Solution-process (some has-input Powder-for-solution-for-injection))))) with

(inverse-role has-product is-product-of) (inverse-role has-input is-input-of) All I could do with this so far was to chase RACER into an infinite cycle. But I don't know how I might relate the two concepts to find out that they are actually the same thing viewed from two different angles.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/ha-mo-we/Racer/issues/21?email_source=notifications&email_token=AB2476WOIUQMGD5UTBIJR2TQAELFXA5CNFSM4ICVI7FKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD2KJWRY#issuecomment-513055559, or mute the thread https://github.com/notifications/unsubscribe-auth/AB2476TIWT47QAYUEU66633QAELFXANCNFSM4ICVI7FA.