Re: Full nonentailment and consistency tests

> On September 11, Jeremy Carroll writes:
> >
> >
> >
> > Last telecon, and on the list, there was discussion how incomplete
> > typically do not prove nonentailments or consistency.
> >
> > We are not expecting complete Full reasoners, so we are not expecting
> > 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.

We have been using that saturation for a long time
(rdfs rules, xsd rules, beginning of owl rules)
but while attempting some particular testcases
(not necessarily complex ones eg extensional ranges)
it wasn't practical anymore and we opted for explicit
non-saturation (eg explicitly looking for facts only)
which is of course not complete and which means that
we can't pass nonentailment and consistency tests.

Jos De Roo, AGFA

Received on Monday, 15 September 2003 17:14:57 UTC