Re: CR/PR questions

[...]

> 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