- From: Thorsten Liebig <liebig@informatik.uni-ulm.de>
- Date: Mon, 19 May 2003 16:53:44 +0200
- To: Jeremy Carroll <jjc@hplb.hpl.hp.com>
- CC: www-webont-wg@w3.org

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