Re: Test Cases: Extended Cardinality Testing

Jeremy Carroll schrieb:
 >
 > Thanks for these comments.
 >
 > We've just voted to move test to last call, so I will add your suggested
 > additional tests after last call publication (probably 28th May).
 >
 > With the additional tests I notice you use relatively small numbers but
 > the paper
 > http://kogs-www.informatik.uni-hamburg.de/~haarslev/publications/m4m2.pdf
 >
 > suggest racer is not constrained by the numbers themselves. Do you know
 > if I am correct in thinking that racer could solve examples similar to
 > the ones you suggest but with much large numbers (100s or 1000s).

I think you are right. The paper you mention states:
"... we also generated a set of benchmarks where the numbers occurring in
the number restrictions are increased in the same way as for the benchmarks
from Figure 3. There is no need to display the results in detail since the
algebraic reasoner can solve these problems in constant time (below 0.4 seconds)
.." (p. 10)
This is in compliance with my tests with cardinality restrictions of 6000
and above.

However, the paper reports about 2^n variables and tests for cardinality
restrictions with many different existential restrictions and one maximum
cardinality restriction like the following:

(concept-satisfiable?
  (and (some r A01) (some r A02) (some r A03) (some r A04)
       (some r A05) (some r A06) (some r A07) (some r A08)
       (some r A09) (some r A10) (some r A11) (some r A12)
       (some r A13) (some r A14) (some r A15) (some r A16)
       (some r A17) (some r A18)
       (at-most 2 r)))

Racer needed over two minutes (and over 500MB main memory) to prove the
satisfiability of the above (when executed the first time).

 > I have some questions about the error you report ...
 >
 > Thorsten Liebig wrote:
 >
 >> I found two bugs in section 7.3.4 Extended Cardinality Testing:
 >>
 >> <description-logic/Manifest902#test>:
 >> The description says:
 >> "This non-entailment can be replicated for any three natural numbers
 >> i, j, k such that i+j < k. In this example, they are chosen as 2, 3
 >> and 6."
 >> but the conclusion is (in Racer syntax):
 >
...
 >
 > I think this is a syntactic misunderstanding.
 > Please send me a URL for your syntax and I will try and speak your
 > language a bit better.

You are right. I have been confused about the form the (non-)entailments
are represented.

In Racer <description-logic/Manifest902#test> would then look like:

(define-primitive-concept A)
(define-primitive-concept B (not A))
(define-primitive-role r)
(define-primitive-role p :parent r :range A)
(define-primitive-role q :parent r :range B)

And the non-entailment can then be proven with:

(concept-subsumes? (at-least 6 r)
		   (and (at-least 2 p) (at-least 3 q)))

Which returns NIL/false.

Nevertheless, some more elaborated tests would make up this part of the
test document. E.g.:

(concept-subsumes? (at-least 2 r)
		   (and (at-least 2 p) (at-most 2 q)))
;; should be true

(concept-subsumes? (at-least 3 r)
		   (and (at-least 2 p) (at-most 2 q)))
;; should be false

(concept-subsumes? (exactly 0 p)
		   (and (at-most 2 p) (at-least 2 q) (all r A)))
;; should be true

Or more complex:

(define-primitive-concept C)
(define-primitive-concept A C)
(define-primitive-concept B (and C (not A)))
(define-primitive-concept D C)
(define-primitive-role r :range C)
(define-primitive-role p :parent r :range A)
(define-primitive-role q :parent r :range B)
(define-primitive-role s :parent r :range D)

(concept-subsumes? (at-least 6 r)
		   (and (exactly 3 p) (exactly 3 q) (exactly 3 s)))
;; should be true

(concept-subsumes? (at-least 7 r)
		   (and (exactly 3 p) (exactly 3 q) (exactly 3 s)))
;; should be false

I could send you the DAML(OWL) export of Racer from the examples above
if this would be helpful for you.

 > If you will be in Budapest next week please look me up (I am staying in
 > the main conference hotel)

Unfortunately, I will not travel to Budapest.

Thorsten

Received on Monday, 19 May 2003 10:57:11 UTC