- 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