- From: Ian Horrocks <horrocks@cs.man.ac.uk>
- Date: Mon, 15 Sep 2003 22:37:54 +0100
- 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 UTC