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

> 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 UTC