Faster Smarter Proof by Induction in Isabelle/HOL

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. https://youtu.be/4umf8Zhjy7c This work, "Faster Smarter Proof by Induction in …

Continue reading Faster Smarter Proof by Induction in Isabelle/HOL

Simple Dataset for Proof Method Recommendation in Isabelle/HOL

Are you curious about machine learning for theorem proving, but don’t know where to start?  Have you heard about those theorem provers with weird names, like Isabelle, Coq, and Lean?  Actually, it’s not just their names. Their internal architectures can be, … how should I say …, overwhelming, too. Isabelle isn’t like Python or R. …

Continue reading Simple Dataset for Proof Method Recommendation in Isabelle/HOL