Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.



I’m puzzled about this. I thought the issue was that flex-flex constraints were suddenly being smashed now, when they were not before. And I would certainly not have wanted every blast call to smash all flex-flex constraints, because this can lose completeness.

Note that flex-flex pairs attach to theorems, and therefore to proof states as a whole, and not to individual subgoals.

Larry

On 10 Dec 2013, at 12:42, Makarius <makarius at sketis.net> wrote:

>> Larry might have had very good reasons to smash the flex-flex pairs in 1998. These reasons might no longer apply, or the experiments so far did not get to the point where the difference is visible.
> 
> Larry, can you give further hints about that?
> 
> Alternatively, someone else can volunteer to make further experiments on all reachable Isabelle applications, to consolidate the empirical findings.  This will only take a few hours.
> 
> In particular the following questions are relevant:
> 
>  * Do flex-flex pairs after invocation of blast actually happen in
>    practice, i.e. does blast proof reconstruction introduce any by
>    itself?
> 
>  * Is there any performance impact on changing the behaviour?  So far
>    the success or failure was not affected, but there were no
>    measurements of timing so far.





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