[isabelle-dev] HOL-IMP very slow
makarius at sketis.net
Wed Feb 12 20:40:59 CET 2014
On Wed, 12 Feb 2014, Jasmin Blanchette wrote:
>>> Metis is a FO ATP developed by Hurd. "metis" is a higher-order proof
>>> method (and tactic) that translates HOL to FOL (like Sledgehammer
>>> does), developed by Paulson & Susanto.
>> Do you understand yourself how that works?
> Does "that" refer to Metis or "metis"? I've never looked much under
> Metis's hood except to tweak its options. For "metis", the answer is a
> qualified yes.
Mainly the proof reconstruction on the Isabelle side, especially the
question of type variables.
See also 568b2cd65d50: the long comment in the source after the change
looks like the recently introduced reform of Thm.bicompose (0fa3b456a267)
might help here, but it didn't. Or maybe I was just confused about 8
different modes of that function. (One of the booleans is only required
for this particular instance, IIRC.)
More information about the isabelle-dev