The main problem with these monsters is that they often don’t work, and related to this, they often “obtain” functions that don’t appear to be necessary. Where monsters do work, they often suggest quite relevant lemmas. Larry
> On 20 Oct 2020, at 15:27, Jasmin Blanchette <[email protected]> wrote: > > On the positive side, veriT outputs detailed proofs (like Z3 but unlike > CVC4), which are parsed by Isabelle and yield these "semi-intelligible Isar > monsters". Some users find that they can fish out useful bits from them, if > not use them as is; others find them too broken or ugly. Improving the > situation here is high on my agenda for Sledgehammer, because it's generally > the key to proof reconstruction for stronger ATPs (e.g. HO). _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
