Proof By Abduction in Isabelle/HOL

• Venue: Seventh Conference on Artificial Intelligence and Theorem Proving (AITP2024)
• Location: Aussois, France
• Authors: Yutaka Nagashima, Daniel Sebastian Goc
• Extended Abstract: https://aitp-conference.org/2024/abstract/AITP_2024_paper_35.pdf
• Slides: https://aitp-conference.org/2024/slides/YN.pdf

Abstract

When proving an inductive problem, we often prove auxiliary lemmas that are useful for proving the original problem. If these auxiliary lemmas themselves are challenging, we must introduce more lemmas to prove these lemmas. To automate such multi-step conjecturing, we developed Abduction Prover. Given a proof goal, Abduction Prover conjectures a series of lemmas and attempts to prove the original goal using these lemmas. Our working prototype of Abduction Prover for Isabelle/HOL is publicly available on GitHub.

Video (Demo)

Video (Seminar)

Mindmap