[isabelle-dev] HOL-IMP very slow

[Jasmin Christian Blanchette]

Am 12.02.2014 um 16:40 schrieb Dmitriy Traytel <traytel at 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.