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

On September 25, Jim Hendler writes:
> 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).

Fair enough. It might be worth mentioning, however, that guide only
mentions one example of oneOf (the definition of WineColor), whereas
the wine ontology uses it extensively.

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

Agreed - proving that our example ontology is consistent is hard work
and is not very interesting.

>   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).

Fine. The obvious thing would be to have sets of inconsistent tests
that import the wine and food ontologies and assert things like "x
hasDrink y", where x is an instance of BlandFishCourse and y is an
instance of a wine that hasFlavor Strong.

Regards, Ian

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

Received on Thursday, 25 September 2003 17:08:39 UTC