Re: Full nonentailment and consistency tests

On September 11, Jeremy Carroll writes:
> 
> 
> 
> Last telecon, and on the list, there was discussion how incomplete reasoners 
> typically do not prove nonentailments or consistency.
> 
> We are not expecting complete Full reasoners, so we are not expecting anyone 
> to prove the Full nonentailments or consistency tests.

This is not correct. It is perfectly possible to have an incomplete
reasoner that can prove some or all of the Full nonentailments or
consistency tests. E.g., many FO provers are "complete" in the sense
that when they saturate their clause set without finding a
contradiction, then they can guarantee that there really is no
contradiction. Similarly, one could imagine running a resolution style
prover looking from inconsistencies in parallel with a model builder
trying to prove consistency by building a model.

The kind of incompleteness you are talking about stems from the fact
that such systems can't guarantee to answer yes/no on all inputs
(e.g., the resolution clause set may continue to grow without ever
saturating, or both prover and model builder may fail).

Regards, Ian


> However, we are expecting such reasoners to not *fail* such tests (i.e. get 
> the wrong answer).
> 
> A fix would be to change our exit criteria to reflect this, however DanC 
> suggested it would be easier to reclassify such tests as extra credit.
> 
> ....
> 
> Looking at it - it is somewhat complicated ...
> 
> Currently the concept of extra credit tests is only introduced in the section 
> of extra credit tests, and the extra credit tests are labelled as informative 
> (even though we could decide that as syntax checker tests they are 
> normative).
> Currently a Full nonentailment test like imports-002
> 
> http://www.w3.org/TR/owl-test/byFunction#imports-002
> 
> is normative.
> 
> ----
> 
> Suggestion:
> 
> 1) change so that all approved tests to be normative (including approved extra 
> credit tests)
> 
> 2) Introduce the concept to extra credit test in a new subsection in
> section 2
> http://www.w3.org/TR/owl-test/#deliverables
> of test.
> 
> e.g.
> 
> 2.2 Extra Credit Tests
> 
> The web ontology working group has seen adequate implementation experience of 
> most of the tests in this document. Some, however, are particularly difficult 
> to implement efficiently. These are labelled as extra credit tests. Such 
> tests indicate the semantics of OWL, but may use features that are not 
> sufficiently widely implemented to provide good interoperability.
> 
> A general case of extra credit tests is that all  OWL Full nonentailments
> and consistency tests are extra credit tests. This is because typical OWL Full
> implementations prove entailments but cannot prove nonentailments.
> 
> Extra credit tests are labelled as such both within this document and in the 
> manifest files.
> 
> The name indicates that there is no expectation that any implementation will 
> successfully run such tests and any that do gain extra credit. 
> 
> 3) Corresponding changes concerning the manifest files
> 
> 4) Adding an "Extra Credit" label (linked to new section 2.2) to every extra 
> credit test.
> 
> 5) Modifying the Testing an OWL Implementation section to clarify that an OWL 
> Syntax Checker must pass extra credit tests.
> 
> 
> Jeremy
>

Received on Monday, 15 September 2003 08:53:39 UTC