Faster Smarter Proof by Induction in Isabelle/HOL

On By yutakang

Do you want to know how to apply proof by induction formally?

This year at IJCAI, I presented my paper about the automation tool for proof by induction in Isabelle/HOL.

Though IJCAI has already finished, you can find my promotion video for this paper on YouTube.

This work, “Faster Smarter Proof by Induction in Isabelle/HOL”, is an improved version of our earlier work “Smart Induction for Isabelle/HOL” at FMCAD2020. I also made a promotion video for this paper.

Thanks to their open access policies, both papers are available for free.

And both papers are based on simple tree-search models.
So, they are approachable for people who are not familiar with Isabelle/HOL.

I hope you enjoy them!