Stream: Isabelle/ML

Topic: Fast Instantiation Method


view this post on Zulip Mathias Fleury (Sep 12 2020 at 08:39):

I have an unusual use case: I check the proofs generated by the SMT solver veriT (so once I have pushed my work, there will be a veriT_smt and an smt tactic). There is one rule that appears very often, namely ?P ≠ ?Q ∨ ¬ ?P ∨ ?Q with some (potentially large) P and Q.

What is the fastest way to convert the term to a theorem? I have tried various things and never managed to get below 10ms (on my computer), but replaying such steps is so trivial that I find 10ms already too much.

Here is a real example if you want to play with it:


Last updated: Jun 20 2024 at 08:21 UTC