- 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
[...] > 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 UTC