Re: [isabelle] Interesting example of blast looping in 2016-1



Your problem is not first-order and therefore lies outside the scope of blast. As I recall, there was a minor change connected with problems of that general sort. That particular example is unfortunate, but it is easily provable using other proof methods, including auto, fast and best.

Larry Paulson


> On 9 Feb 2017, at 04:30, Rafal Kolanski <xs at xaph.net> wrote:
> 
> Hello,
> 
> When updating one of our branches to 2016-1 I came across blast looping
> on this subgoal when it did not do so previously:
> 
> âjâset w. Â j â True â set w
> 
> Interestingly, blast is OK with this one:
> 
> âjâset w. Â j = True â True â set w
> 
> and also
> 
> âjâset w. j = False â True â set w
> 
> Any ideas what changed to cause this? In this case I switched over to
> fastforce due to being in a hurry, but it would be useful to understand
> for future reference.
> 
> Sincerely,
> 
> Rafal Kolanski
> 
> 




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