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

Re: CR/PR questions

From: Jeremy Carroll <jjc@hpl.hp.com>
Date: Mon, 5 May 2003 22:14:13 +0300
To: www-webont-wg@w3.org
Message-Id: <200305052214.13579.jjc@hpl.hp.com>

> If your contention is that there are some things for which current 
> systems can handle, but optimizations will be needed for larger 
> community acceptance, I probably wouldn't disagree, but also wouldn't 
> think these hold up the move to PR  - optimizations generally come 
> later in the day for these sorts of specs - what's more, there are 
> already a couple of implementations where it appears to me that OWL 
> reasoners can call out to other processes for doing artihmetic (or 
> anything else for which there is a well-known process that is believe 
> to be logically consistent) and thus it is a question of these being 
> cited and more integrated.

One of my contentions is that there are *easy* OWL DL tests that no currently 
implemented system can solve.
This points to one of two things:
- work that needs to be done by implementors to get their systems to do more
- work needed by the editors to make it clear that just because you can do 
some reasoning in your head that does not mean that you should expect an OWL 
reasoner to do it. (OWL Full has some health warnings about no complete 
reasoners but I am not aware of any for OWL DL).

*can* means before the heat death of the universe, rather than in some longer 
time frame.

The tests I have been working today, fit that pattern.

These can be done in my head, because I can reason about the cardinalities of 
classes. An OWL DL reasoner which does not have this ability is severely 
challenged. Either we should make it clear that users should not expect 
reasoners to have this ability, or we should have tests that exercise these 
abilities, and wait in CR until reasoners can pass them.

I take the well known pattern of 1-to-N relationships from UML, and encode 
them in OWL, as relationships between finite sets.

An easy (soluble) example is:
  I take a singleton class., I take a 1-to-2 relationship between that and a 
second class. I take a 1-to-3 relationship between that and a third class, 
now I add a 1-to-6 relationshup between the first class and the third class.
This is consistent.

If I increase the numbers, to beyond what one count on ones fingers I will 
challenge most systems severly 200, 300, 60000 - not in themselves 
unreasonable numbers. For me, to do in my head, it does not make the problem 
much harder.

If I replace the 6 with a 5 then the file is inconsistent.
Now, I can replace the original singleton set with an infinite set, and 
because infinity*2*3 = infinity*5 the ontology is now consistent.
Using a maxCardinality constraint with some large number I can instead insist 
that the first class is finite, but I don't really know what. Since the size 
of the original class has no bearing on the arithmetic it does not matter.

The tests I have been working on are found in

http://www.w3.org/2002/03owlt/editors-draft/draft/proposed-dl-900-arith

In the abstract syntax these are:

905
individualValuedProp( #p-N-to-1 
          inverse( #invP-1-to-N ) 
          domain( #cardinality-N )
          range( #only-d )
          Functional )
individualValuedProp( #q-M-to-1 
          inverse( #invQ-1-to-M) 
          domain( #cardinality-N-times-M )
          range( #cardinality-N )
          Functional )
individualValuedProp( #r-N-times-M-to-1 
          inverse( #invR-1-to-N-times-M) 
          domain( #cardinality-N-times-M )
          range( #only-d )
          Functional )
EnumeratedClass( #only-d { #d } )
EquivalentClass( #only-d 
        restriction( #invP-1-to-N cardinality=2 )
        restriction( #invR-1-to-N-times-M cardinality=6 )
       )

EquivalentClass( #cardinality-N
        restriction( #p-N-to-1 someValuesFrom(#only-d) )
        restriction( #invQ-1-to-M cardinality=3 )
       )
EquivalentClass( #cardinality-N-times-M
        restriction( #r-N-times-M-to-1 someValuesFrom(#only-d) )
        restriction( #q-M-to-1 someValuesFrom(#cardinlaity-N) )
       )
 

906 is the same but with the numbers increased to 20, 30 600,
907 ditto but 200, 300, 60000

908 is also consistent, it seems similar and wrong at first blush:


908
individualValuedProp( #p-N-to-1 
          inverse( #invP-1-to-N ) 
          domain( #cardinality-N )
          range( #infinite )
          Functional )
individualValuedProp( #q-M-to-1 
          inverse( #invQ-1-to-M) 
          domain( #cardinality-N-times-M )
          range( #cardinality-N )
          Functional )
individualValuedProp( #r-N-times-M-to-1 
          inverse( #invR-1-to-N-times-M) 
          domain( #cardinality-N-times-M )
          range( #infinite )
          Functional )
EquivalentClass( #infinite 
        restriction( #invP-1-to-N cardinality=2 )
        restriction( #invR-1-to-N-times-M cardinality=5 )
       )

EquivalentClass( #cardinality-N
        restriction( #p-N-to-1 someValuesFrom(#infinite) )
        restriction( #invQ-1-to-M cardinality=3 )
       )
EquivalentClass( #cardinality-N-times-M
        restriction( #r-N-times-M-to-1 someValuesFrom(#infinite) )
        restriction( #q-M-to-1 someValuesFrom(#cardinlaity-N) )
       )

The number 6 has been replaced by 5, and the class only-d has been renamed as 
infinite; and the enumerated class axiom has vanished. This system has 
infinite models only. I would be disappointed if FACT can't do this one 
today.

Test 910 is simply an inconsistent variant of 907.
Test 909 is more interesting, in that it is based on 908, but with the class 
named #infinite renamed as #finite and then limited in size using another 
property and a maxCardinality constraint.

910:
individualValuedProp( #p-N-to-1 
          inverse( #invP-1-to-N ) 
          domain( #cardinality-N )
          range( #finite )
          Functional )
individualValuedProp( #q-M-to-1 
          inverse( #invQ-1-to-M) 
          domain( #cardinality-N-times-M )
          range( #cardinality-N )
          Functional )
individualValuedProp( #r-N-times-M-to-1 
          inverse( #invR-1-to-N-times-M) 
          domain( #cardinality-N-times-M )
          range( #finite )
          Functional )
EquivalentClass( #finite 
        restriction( #invP-1-to-N cardinality=2 )
        restriction( #invR-1-to-N-times-M cardinality=5 )
        restriction( #f-K-to-1 someValuesFrom( #only-d ) )
       )

EquivalentClass( #cardinality-N
        restriction( #p-N-to-1 someValuesFrom(#infinite) )
        restriction( #invQ-1-to-M cardinality=3 )
       )
EquivalentClass( #cardinality-N-times-M
        restriction( #r-N-times-M-to-1 someValuesFrom(#infinite) )
        restriction( #q-M-to-1 someValuesFrom(#cardinlaity-N) )
       )
individualValuedProp( #f-K-to-1 
          inverse( #invF-1-to-K) 
          domain( #only-d )
          range( #finite )
          Functional )


EnumeratedClass( #only-d { #d } )
EquivalentClass( #only-d 
        restriction( #invF-1-to-K maxCardinality=10000000000 )
       )
Received on Monday, 5 May 2003 16:14:04 GMT

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