Re: Guide tests

On October 8, Jeremy Carroll writes:
> 
> 
> 
> Jeremy:
> 
> >>I am not sure what Martin's current position is - merely that without a 
> >>single implementation passing these two tests that the response given 
> >>during LC is invalidated.
> >>
> 
> 
> Ian: 
> > Surely you can't be serious! It has always been crystal clear
> > (including in our responses to LC comments) that we don't currently
> > have a decision procedure for OWL DL (we removed the definition of
> > "complete OWL Lite consistency checker" from test for this reason).
> > The inability of existing implementations to reliably prove the
> > consistency of OWL DL ontologies is an obvious consequence of this
> > fact. Moreover, the spec allows conforming consistency checkers to
> > return "Unknown" when they are unable to determine if a document is
> > consistent or inconsistent.
> > 
> 
> 
> Of course you are right that there was much in the response that remains 
> pertinent, and requesting reopening discussion is not intended as a 
> free-for-all.
> 
> However text such as
> 
> [[
> The WG has been made aware of implementations of OWL DL that include
> both inverseOf and oneOf and which seem to be performing well in
> practice.  The working group will definitely consider their status
> and usability before deciding on our schedule with respect to
> Candidate Recommendation and Proposed Recommendation.
> ]]
> 
> suggests that straightforward examples including both features should be 
> tractable.

Firstly, the problem arises with the combination of inverseOf, oneOf
and *counting* (i.e., cardinality restrictions).

Secondly, tractability isn't the issue - it is completeness. Our new
reasoner has no trouble dealing with the Wine ontology via the
translation of instances into concepts. Using this translation,
however, means that it is sound but incomplete
w.r.t. unsatisfiability, so failing to prove unsatisfiability means
"don't-know". 

Most/all of the existing implementations are similarly better at
proving unsatisfiability, but there is no reason in principal why
someone can't build a reasoner that is sound but incomplete
w.r.t. satisfiability, i.e., it can prove satisfiability (e.g., by
building a model), but failure to prove satisfiability means
"don't-know". I imagine that such a system would easily pass this test
as the ontology has quite a simple structure, and there should be many
possible models.


> 
> The decisions made about what was in DL were known to be pushing the 
> boundaries, and the changes we made during LC reflect that we were not 
> expecting implementations to be able to pass maybe some of the more 
> difficult DL tests (e.g. 3-sat encoded with oneof).
> 
> The guide examples, in contrast, are not attempting to be clever or to be a 
> challenge to systems, merely exemplory use of DL.

We already covered this. The example isn't necessarily realistic as it
(quite reasonably) tries to cover all aspects of the language. We
always knew that ontologies using all aspects of the language
simultaneously (in particular, inverseOf, oneOf and counting) would be
difficult to deal with.


> 
> As far as I can tell, most of my colleagues see the current failure to 
> prove these tests as justifying our earlier scepticism about the usefulness 
> of the DL boundary, but accept that given where we are in the process, the 
> likely outcome will be adequate text in the guide exlaining how to remain 
> within a smaller more tractable subset.

There is still considerable utility in the fact that we can reason
effectively with most combinations of constructors - I think that this
is illustrated very nicely by the tests, where many systems are able
to pass both consistent and inconsistent tests with relative
ease. Moreover, the fact that DL is still decidable gives reasonable
hope that the existing techniques can be extended to the whole
language - several groups of logicians are working on this problem,
and I am confident that a "practical" algorithm will be developed in
the near future.

Ian


> 
> Jeremy
> 
> 
> 
>

Received on Wednesday, 8 October 2003 09:36:26 UTC