Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Induction proofs with Vampire

view this post on Zulip Email Gateway (Aug 22 2022 at 21:08):

From: Buday Gergely <buday.gergely@uni-eszterhazy.hu>
Hi,

I learned that auto is using Vampire and that Vampire is starting to handle
induction automatically. Is this used in auto? If not, are there plans to
incorporate?

view this post on Zulip Email Gateway (Aug 22 2022 at 21:09):

From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi Gergely,

That's currently not used in Isabelle, although it could be a useful addition. The natural place for it would be Sledgehammer, not auto, though. ;)

Cheers,

Jasmin

Last updated: Apr 24 2024 at 20:16 UTC