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