Re: the MPTC Dilemma (please solve)

On Tue, Feb 21, 2006 at 03:50:52PM +0800, Martin Sulzmann wrote:

A depth limit is not enough. For confluence we need that *all* derivations for a particular goal terminate. Once we have confluence we get completeness of the inference checks.

So without a static test for termination (though just for this goal), we're still in the no-man's land between proof and counterexample. Reduction might be confluent, but we have no proof.