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

Re: CR/PR questions

From: Jos De_Roo <jos.deroo@agfa.com>
Date: Tue, 6 May 2003 00:21:07 +0200
To: "Jim Hendler <hendler" <hendler@cs.umd.edu>
Cc: Jeremy Carroll <jjc@hpl.hp.com>, www-webont-wg@w3.org, www-webont-wg-request@w3.org
Message-ID: <OFC534FDF8.6EA81338-ONC1256D1D.0078CA00-C1256D1D.007ACBD6@agfa.be>


[...]

> several implemented reasoners can solve any decidable problem, but
> have either physical restrictions (like running out of memory) or
> heuristic limits (like Jos's restrictions in Euler as to when to cut
> off search) - I guess I don't understand why this wouldn't count as
> implementing our system or needing an infinitely long CR.

I was wondering if you were talking about the same Euler ;-)
We believe that following holds for the Euler path detection
Solution Lemma II:
Be C the set of all closure paths that generate solutions,
then there exist matching resolution paths that generate
the same solutions.
(or no solutions are excluded) and
Infnite Looping Path Lemma:
If the closure graph G' is not infinite and the resolution
process generates an infinite number of looping paths then
this generation will be stopped by the anti-looping technique
and the resolution process will terminate in a finite time.

However what we can do is terminate it manually (or set
a maximum step count, but that is not very heuristically ;-)

Anyhow, I agree with your main argument Jim.


-- ,
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
Received on Monday, 5 May 2003 18:21:35 GMT

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