[...] > 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.29 : Thursday, 27 January 2005 18:05:00 GMT