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.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
