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 logic sense, not in the
Isabelle sense). The Metis prover, like most if not all ATPs, is sensitive to
the (relative order of the) names of the symbols -- e.g. it may apply different
rules in a different order.
It would be possible, and indeed a good idea, to insulate ourselves from this
by having the "metis" proof method name Skolems serially ("sk1", "sk2", etc.)
before invoking the Metis prover [*]. This would probably trigger a couple of
bad cases like we saw today, but as a result we would be immune from the
disease. I'll think about this.
Jasmin
[*] Subtle terminology point: 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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
