[isabelle-dev] Metis: Unused Theorem Reduces Run-Time?
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Fri Jan 18 19:29:16 CET 2013
Am 18.01.2013 um 16:44 schrieb Tjark Weber:
> The new AFP entry on Kleene Algebras contains a metis call
> that generates a warning about an unused theorem local.opp_mult_def.
> Not passing opp_mult_def as an argument to metis gets rid of the
> warning, but increases run-time of this metis call from ~ 1 s to ~ 15 s
> on my machine.
Sure, these things happen with pretty much any tool that performs a heuristic search. There are even (rare) cases where taking out the unused theorems will lead to an unprovable first-order problem (because of incompletenesses in the translation of HO constructs).
What's your concrete suggestion here?
More information about the isabelle-dev