Re: Test Cases: Extended Cardinality Testing

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 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):
> 
> (define-primitive-concept nonconclusions902
>   (and (at-least 2 p)
>        (at-least 3 q)
>        (at-least 6 r)))
> 
> which is indeed satisfiable.
> I suppose the following conclusion was intended:
> 
> (define-primitive-concept nonconclusions902
>   (and (at-least 2 p)
>        (at-least 3 q)
>        (at-most 4 r)))
> 
> But since at-most represents a "less or equal" condition
> (http://www.w3.org/TR/owl-semantics/direct#owl_maxCardinality_semantics)
> the description should then say "... i, j, k such that i+j =< k. In this
> example, they are chosen as 2, 3 and 4."
> 


I have looked at the test and believe it to be valid non-entailment.

Consider an interpretation that has


denotes A with a class with extension { a1, a2 }
         B  ....               .....   { b1, b2, b3 }
and a further individual  i,
where these six individuals are distinct
and
p is a property with extension
< i a1 >, < i a2 >

q is a property with extension
< i b1 > < i b2 > < i b3 >

and r is the union of p and q.

then

i is in (at-least 2 p)

i is in (at-least 3 q)

but

i is not in (at-least 6 r)

showing that the intersectionOf (at-least 2 p) and (at-least 3 q) is not a 
subclassof (at-least 6 r)


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.

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


> The same is to <description-logic/Manifest904#test>.
> 
> BTW: the current tests are not very sophisticated. I suggest
> to add more complex cardinality test.
> 
> E.g. the following entailments:
> 
> (define-primitive-concept conclusion-x1
>   (and (at-least 2 p)
>        (at-most 2 q)
>        (exactly 3 r)))
> 
> (define-primitive-concept conclusion-x2
>   (and (at-most 2 p)
>        (at-least 4 r)
>        (at-most 2 q)))
> 
> (define-primitive-concept conclusion-x3
>   (and (at-most 2 p)
>        (at-least 4 r)
>        (all r A)
>        (at-least 3 q)))
> 
> Or even 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)
> 
> (define-primitive-concept conclusion-x4
>   (and (exactly 3 p)
>        (exactly 3 q)
>        (exactly 3 s)
>        (at-most 6 r)))
> 
> And some corresponding non-entailments.
> 
> Thorsten
>

Received on Friday, 16 May 2003 12:00:28 UTC