[isabelle-dev] AFP: PAPP_Impossibility not terminating
makarius at sketis.net
Tue Apr 18 11:04:53 CEST 2023
On 18/04/2023 10:07, Manuel Eberl wrote:
> I did notice at the time that the vast majority of the time was spent in
> taking the union of the hyps of the different theorems being combined, so I
> made sure that when I create the theorems, they all have pointer-equal hyps,
> which sped things up phenomenally.
Did you re-invent this yourself, or did you see it here?
> I should also still have a few smaller example applications of
> that SAT solver lying around that one could use; there the difference between
> the old and the new version would perhaps not be "2 minutes" vs
> "non-termination" but rather something like "almost instant" and "half a
> minute" or so, which may make debugging less painful.
It would be great to have such small benchmark examples. Please send them to
More information about the isabelle-dev