W3C home > Mailing lists > Public > www-webont-wg@w3.org > September 2003

Re: Full nonentailment and consistency tests

From: Ian Horrocks <horrocks@cs.man.ac.uk>
Date: Mon, 15 Sep 2003 22:37:54 +0100
Message-ID: <16230.12594.992064.166747@merlin.horrocks.net>
To: "Jos De_Roo" <jos.deroo@agfa.com>
Cc: Jeremy Carroll <jjc@hpl.hp.com>, www-webont-wg@w3.org

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/
> 
Received on Monday, 15 September 2003 17:39:50 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:58:02 GMT