Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk:
I’m not sure what the question is any more. If it is about the choice of
names in Skolemization, that has been entirely redone in the past few years.
I imagine it is now something like this:
Subgoal.FOCUS (fn
I know it was a problem for machine learning that a free variable in a goal (x
say) might appear with multiple types in a problem set. This is connected with
the issue you’re describing now. I assume that that was solved somehow.
Larry
On 13 Feb 2014, at 12:31, Jasmin Blanchette
On Thu, 13 Feb 2014, Jasmin Blanchette wrote:
Am 13.02.2014 um 13:19 schrieb Lawrence Paulson l...@cam.ac.uk:
I’m not sure what the question is any more. If it is about the choice
of names in Skolemization, that has been entirely redone in the past
few years. I imagine it is now something
Tests about slowness take long, but here is a presumably good point in the
published history:
Isabelle/db691cc79289
Finished Pure (0:00:10 elapsed time, 0:00:12 cpu time, factor 1.20)
Finished HOL (0:02:13 elapsed time, 0:05:56 cpu time, factor 2.67)
Finished HOL-IMP (0:01:58 elapsed time,
Should be fine again (or at least better) with b445c39cc7e9. Thanks for
the notification.
Dmitriy
Am 12.02.2014 16:28, schrieb Makarius:
Tests about slowness take long, but here is a presumably good point in
the published history:
Isabelle/db691cc79289
Finished Pure (0:00:10 elapsed time,
Am 12.02.2014 um 16:40 schrieb Dmitriy Traytel tray...@in.tum.de:
Should be fine again (or at least better) with b445c39cc7e9. Thanks for the
notification.
For the record: The goal state before and after had different variable names in
it. These become Skolem constants to Metis (in the FO
Am 12.02.2014 um 16:03 schrieb Makarius makar...@sketis.net:
I see a lot of incoming changes (and many hg queue accidents) just before
that,
The accidents were that I experimented with qfold for the first time. The
command merges two patches together. The patches themselves were all as I
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
Am 12.02.2014 um 20:40 schrieb Makarius makar...@sketis.net:
Mainly the proof reconstruction on the Isabelle side, especially the question
of type variables.
I can't help much there. Perhaps Larry knows more. All I can recall is that
Metis sometimes suggests type instantiations (since types
