Re: Chair's Concerns re: Test Cases and CR

At 10:31 AM +0100 9/25/03, Ian Horrocks wrote:
>On September 24, Jim Hendler writes:
[snip]

>>  - however, two of them are:
>>
>>  [Results] miscellaneous-001 levels:DL, Full [APPROVED: Med L XXL]
>>  Wine example taken from the guide.
>>
>>  [Results] miscellaneous-002 levels:DL, Full [APPROVED: Med L XXL]
>>  Food example taken from the guide.
>
>Both these ontologies are in DL, mainly because they use the oneOf
>constructor. As they also use cardinality constraints and inverse
>properties, they are in that fragment of the language for which we
>know that we don't currently have a practical decision procedure
>(i.e., a sound, complete and terminating consistency testing
>algorithm). For this language, all of the existing systems are (at
>best) sound but incomplete w.r.t. *inconsistency*, i.e., they can
>sometimes prove inconsistency, but if they fail to do so then we know
>nothing.  Given that the tests in question are consistency tests, none
>of these systems can be expected to report pass.
>
>Note that it would in principal be possible to design an algorithm
>that was sound but incomplete for *consistency* in this language, but
>I don't know of anyone who is working on this aproach.
>
>If the use of individuals in oneOf constructs is eliminated in favour
>of unions of classes, then the ontologies could (in principal) be
>proved consistent by several of the existing systems. (In fact with
>such a modification we are able to completely classify the wine
>ontology in about 10s and the food ontology in less than 1s using the
>latest version of the FaCT++ system.) I believe that we should make
>such a change: the extensive use of oneOf in the wine and food
>ontologies is largely gratuitous (it seems to be mainly the result of
>their origin in a language that supported this constructor but did not
>support unions of classes), and is setting a bad example to
>prospective users - it encourages the use of statements that are, in
>most cases, stronger than is needed/intended, and that are known to be
>difficult to reason with.
>
>One further point. Given the elimination of oneOf, then the wine and
>food ontologies could even be transformed into OWL Lite, although this
>would result in some mangling of the syntax (in order to capture
>negation and disjunction).
>
>Regards, Ian
>
>

I definitely would oppose "recoding" these tests unless we also 
rewrote the Guide to match, and it strikes me that that would be a 
lot of work at this late stage, and might even be deemed by some to 
be a design change (I don't think it would be, but I don't want to 
even open the door the slightest bit to that criticism).

Seems to me therefore that the problem may be that we are doing these 
as consistency rather than entailment tests -- given that they use 
features that we know are hard for DL reaoners, it strikes me as a 
place where the rule-based, incomplete reasoners might be able to 
show what they could do-- but many of those can prove entailments 
rather than inconsistencies -- and, in fact, rereading the Guide I 
realize that a more typical query would be something like
   "From the current ontology can we conclude that WINE1 goes well 
with FOOD1", as opposed to asking "Is the whole wine ontology 
consistent"

  What I would suggest would be to create a version of these tests 
that are entailment tests (by generating a number of different 
conclusions that are entailed from the current set) -- we would 
therefore not be changing the ontology that shows up in the Guide at 
all -- and ADDing these to the test set.  I would also think we might 
consider taking the two current approved tests and making them extra 
credit (since we would have the new entailment tests added to show 
these features of OWL are usable).

This would have two desirable effects - it would create a couple of 
harder tests for "incomplete" OWL systems like Surnia and Euler to be 
tested on (or, for example, my group is playing with a rule-based OWL 
Full tool, and finds our current test set pretty unexciting), and it 
would create a couple of tests (in the extra credit camp) to motivate 
the folks in the theorem proving community to shoot for (i.e. we 
would motivate the search for an effective procedure in the decidable 
set where transitive and oneOf both are used -- the bragging rights 
for the first folks to solve our test would be high!)

  -JH




-- 
Professor James Hendler				  hendler@cs.umd.edu
Director, Semantic Web and Agent Technologies	  301-405-2696
Maryland Information and Network Dynamics Lab.	  301-405-6707 (Fax)
Univ of Maryland, College Park, MD 20742	  *** 240-277-3388 (Cell)
http://www.cs.umd.edu/users/hendler      *** NOTE CHANGED CELL NUMBER ***

Received on Thursday, 25 September 2003 11:11:22 UTC