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

Re: Full nonentailment and consistency tests

From: Jos De_Roo <jos.deroo@agfa.com>
Date: Mon, 15 Sep 2003 23:14:12 +0200
To: Ian Horrocks <horrocks@cs.man.ac.uk>
Cc: Jeremy Carroll <jjc@hpl.hp.com>, www-webont-wg@w3.org
Message-ID: <OF3A0DDCBA.DC73DFF2-ONC1256DA2.0072C81D-C1256DA2.0074A7BD@agfa.be>

> 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 http://www.agfa.com/w3c/jdroo/
Received on Monday, 15 September 2003 17:14:57 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:56:55 UTC