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 <jasmin.blanche...@gmail.com> 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 like this:
>>
>> Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
>> EVERY1 [skolemize_prems_tac ctxt negs,
>> Subgoal.FOCUS (cltac o mkcl o #prems) ctxt'])
>> ctxt 1]) i st
>>
>> (I found this in meson.ML.)
>>
>> The original version made little use of contexts, as I recall.
>
> I was a bit confused when I wrote about "skolemization" being the culprit.
> The problem is that fixed variables occurring in the conjecture end up
> keeping their names (modulo some slight alterations). After all, such
> variables are for all practical purposes just like constants. By "fixed"
> variables, I mean among other things the "parameters" of the goal (those
> entites which "rename_tac" works on).
>
> That "metis" performance is affected by the naming of constants is not
> surprising to anybody who knows a thing or two about automated reasoning, but
> it is surprising that even the goal parameter naming affects it.
>
> Jasmin
>
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
