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.
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
> * 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