We're thrilled to announce that our proposal for the 5th International Workshop on Automated (Co)Inductive Theorem Proving (WAIT2024) has been officially accepted for IJCAR 2024! For more information, visit the website: WAIT2024

For a week, I have been feeling devastated reading and watching news from the Middle East. I am deeply concerned for the hostages and victims of the ongoing violence in Israel and the Gaza Strip, as well as other affected areas. I regret not showing more solidarity sooner with the Palestinian civilians who have endured …

Continue reading A statement on the current situation in the Middle East

Hey there! 🎉 Ready for some exciting updates? Dive into this video as we showcase the latest advancements of our Abduction Prover! We're stacking it up against Sledgehammer using 10 riveting inductive challenges from the Tons of Inductive Problems. 🚀 https://youtu.be/rXU-lJxP_GI Here's what's fresh out of the oven this release: 🚦 Unveiled the Best-First Expansion, …

Continue reading Abduction Prover vs Sledgehammer: The Prod Trial

Explore the enhanced capabilities of the Abduction Prover within Isabelle/HOL in our latest demo. Dive deep into the upgraded features of our "goal-oriented conjecturing" tool, first unveiled at CICM20181. Key Innovations in the Abduction Prover for Isabelle2022: 🔍 Efficiently proves goals within Isabelle, crafting insightful conjectures. 🔗 Offers sophisticated analyses of inter-conjecture dependencies. 🌀 Enables …

Continue reading Proof by Abduction, August 2023

Dear colleagues, I am thrilled to announce that our paper, "Template-Based Conjecturing for Automated Induction in Isabelle/HOL," has been accepted for presentation at the 10th IPM International Conference on Fundamentals of Software Engineeringhttp://fsen.ir/2023/. In this paper, we propose a novel approach to automated induction in Isabelle/HOL, using template-based conjecturing. Our method significantly reduces the proof …

Continue reading Template-Based Conjecturing for Automated Induction in Isabelle/HOL

This year, I presented my domain-specific language, SeLFiE, and the concept it implements at TAP2022. Proof assistants offer tactics to apply proof by induction, but these tactics rely on inputs given by human engineers. To automate this laborious process, we developed SeLFiE, a boolean query language to represent experienced users’ knowledge on how to apply the induct tactic …

Continue reading Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction

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

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 …

Continue reading United Reasoning on YouTube

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

Thanks for joining me! This is the first entry of this blog.