Abduction Prover in Isabelle/HOL - Automated Theorem Proving and Conjecturing

Explore the development of an abduction prover in Isabelle/HOL through this insightful 50-minute lecture by Yutaka Nagashima at the Hausdorff Center for Mathematics. Gain valuable lessons in life and delve into the intricacies of Isabelle as the speaker demonstrates the prover's functionality. Learn about the conjecturing process, including its steps and results, while witnessing a live demo of the tool in action. Discover how this innovative approach to theorem proving can enhance your understanding of formal methods and automated reasoning.

Introduction
About me
Lessons of life
Isabelle
Demo
How it works
Conjecturing
Conjecturing Steps
Results