Hi there! We opened our YouTube channel for United Reasoning. At this moment we have only one video available. In this first video, we introduce smart induction for Isabelle/HOL for FMCAD2020. In the coming months we plan to add more videos to present various approaches to improving theorem proving using artificial intelligence.We hope that our video contents make …
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
The Journey Begins
Thanks for joining me! This is the first entry of this blog.
