[isabelle-dev] AFP: PAPP_Impossibility not terminating

Makarius 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 
me privately.


More information about the isabelle-dev mailing list