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

Shouldn't there be errors if forms are not supported by TBox language? #22

Open gschadow opened 5 years ago

gschadow commented 5 years ago

Hi, I have just spent over 3 days to figure out a very puzzling behavior.

Here is the example as simple as I could make it

(delete-all-tboxes)

; BEGINNING OF CASE

(implies-role has-direct-content has-content)
(transitive has-content)
(implies-role (has-content has-ingredient) has-ingredient)

(implies Product Material)
(implies Ingredient Material)
(disjoint Product Ingredient)

(equivalent Product (some has-ingredient Ingredient))

; Now we do some checks:

(concept-subsumes? Product
           (some has-direct-content
             (some has-direct-content
                   (some has-ingredient Ingredient)))) ; => T, good
(concept-subsumes? (some has-ingredient Ingredient)
           (some has-direct-content
             (some has-direct-content
                   (some has-ingredient Ingredient)))) ; => T, good
(concept-subsumes? Material
           (some has-direct-content
             (some has-direct-content
                   (some has-ingredient Ingredient)))) ; => T, good

; and we determine the TBox language

(get-tbox-language) ; => SR

; But now I am adding one more axiom, here, a GCI axiom

(implies (and Product
          (exactly 1 has-state-of-matter Liquid-state-of-matter))
     (some has-wrapping Waterproof-wrapping))

; which changes the TBox language

(get-tbox-language) ; => SRIQ

; so that the conduction of the has-ingreident role through the transitive has-content role no longer workds

(concept-subsumes? Product
           (some has-direct-content
             (some has-direct-content
                   (some has-ingredient Ingredient)))) ; => NIL, wrong!
(concept-subsumes? (some has-ingredient Ingredient)
           (some has-direct-content
             (some has-direct-content
                   (some has-ingredient Ingredient)))) ; => NIL, wrong!
(concept-subsumes? Material
           (some has-direct-content
             (some has-direct-content
                   (some has-ingredient Ingredient)))) ; => NIL, wrong!

; END OF CASE

Shouldn't there be some sort of warning / error output that says that because role cardinality restriction is used, the transitive role composition is no longer being considered?

gschadow commented 5 years ago

Here an even simpler case:

(delete-all-tboxes)
(get-tbox-language) ; => "L-"
(transitive has-content) ; => T
(get-tbox-language) ; => "L-"
(implies-role has-direct-content has-content) ; => (HAS-CONTENT)
(get-tbox-language) ; => "L-H"
(implies-role (has-content has-flavor) has-flavor) ; => ((HAS-CONTENT HAS-FLAVOR))
(get-tbox-language) ; => "L-R"
(concept-subsumes? (some has-flavor X)
 (some has-direct-content
   (some has-direct-content 
     (some has-flavor X)))) ; => T, good
(get-tbox-language) ; => "L-R"
(functional has-flavor) ; => T
(get-tbox-language) ; => "ELRf"
(concept-subsumes? (some has-ingredient Ingredient)
 (some has-direct-content 
   (some has-direct-content
     (some has-ingredient Ingredient)))) ; => NIL, sad
(concept-subsumes? (some has-ingredient Ingredient)
 (some has-direct-content
   (some has-ingredient Ingredient))) ; => NIL, even sadder

None of the role composition works.

It is so severe, that the very moment I introduce any role as functional (functional has-foobar) even if it is not used anywhere else, immediately the role composition logic is broken. But without any warning.