W3C home > Mailing lists > Public > www-webont-wg@w3.org > January 2003

Re: The Ugly Test

From: Jeremy Carroll <jjc@hpl.hp.com>
Date: Wed, 29 Jan 2003 08:17:33 +0100
To: www-webont-wg@w3.org
Message-Id: <200301290817.33320.jjc@hpl.hp.com>

> after a exhausting day I hoped to find some compensation

Proving tests is light relief?

> (the range of p is a
> class with one element and i is in a restriction on property
> p with mincardinality of 1) so can someone give a hint?

Try exhaustive search ...

if S is a set with small cardinality then

x memberOf S
can be rewritten as
x = s1 or x = w2 or ... or x = sn

The hard bit - a test I've yet to write - is when the cardinality of S is not 
so small e.g. 30, but some of the members fit one pattern, some of the 
members fit a second, and the rest a third.

By hand you prove it
define S1 = first pattern
define S2 = second pattern
define S3 = third pattern
S = S1 union S2 union S3

x member of S
rewrites as
x member of S1 or x member of S2 or x member of S3

But ... if you have the exhaustive rule above, you can easily find yourself 
exploring 30 possibilities where almost all the work is essentially the same 
(where by hand one would say 'similarly' and be done with it).

Jeremy
Received on Wednesday, 29 January 2003 02:24:17 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:57:57 GMT