Re: [isabelle] blast looping and backtracking



I don’t think that there is a simple explanation. In general, blast is an instance of a sort of technology that will keep trying if there is anything it can do, and therefore can be expected to loop rather than to terminate with failure.

It would be more concerning to see examples that loop even though there is a proof (in logic, not something involving arithmetic say). And I am sure such examples also exist.

Larry Paulson

> On 26 Nov 2021, at 11:07, Kevin Kappelmann <kevin.kappelmann at tum.de> wrote:
> 
> Thanks Larry - do you also happen to know why blast stops looping if we
> were to swap the cases in the first example I posted? That would maybe
> help me to tag lemmas in a way that makes auto and blast more predictable.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.