Re: [isabelle] The Incredible Proof Machine



Dear Christian,

Am Freitag, den 25.09.2015, 11:13 +0200 schrieb Christian Sternagel:
> 2) Since you mentioned the nice paper by Tobias (on higher-order
> pattern unification). Did you also implement the "devar" optimization
> of the same paper? Just recently, Julian Nagele (a PhD student in our
> group; who I also CC'ed), stumbled upon a problem with "devar" when
> implementing the same algorithm. I do not remember the details (maybe
> Julian could comment), only that a little bit of hg-digging revealed
> the following changeset:
> 
> changeset:   12232:ff75ed08b3fb
> user:        berghofe
> date:        Mon Nov 19 17:34:02 2001 +0100
> summary:     Replaced devar by Envir.head_norm
> 
> (referring to src/Pure/pattern.ML)
> 
> I'm curios to whether others already had a similar experience with
> "devar" and what the intention behind this change was?

Are you referring to âÂ9 Minimizing new variablesâ in the paper? Since
this seems to be part of the ML code in 
http://www21.in.tum.de/~nipkow/pubs/lics93-alpha.ML which I based my
implementation on, I also have that. If there is anything wrong with
it, Iâd like to know of course!

Thanks,
Joachim
-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.