Re: Full nonentailment and consistency tests

On September 15, Jos De_Roo writes:
> 
> 
> Ian:
> > 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.
> 
> 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.

Of course it is necessary to prove that relying on saturation for
nonentailment/consistency results does not compromise soundness. This
is, in general, highly non-trivial.

Ian

> 
> 
> --
> Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
>