Email Gateway (Aug 30 2023 at 21:27): Email Gateway (Aug 30 2023 at 21:27):From: Yutaka Nagashima <united.reasoning@gmail.com>
Dear Isabelle Community,
I'm excited to share the progress of our project, the Abduction Prover
for Isabelle/HOL. It's now approaching a mature stage, designed to
efficiently prove goals, while simultaneously generating and
validating vital auxiliary lemmas.
To provide a clearer picture, I've prepared a video comparison between
the Abduction Prover and Sledgehammer, focusing on select challenges
from the 'Tons of Inductive Problems' set:
Watch the Video Comparison here:
https://www.youtube.com/watch?v=d7IXk0vB2p0
My ongoing efforts aim to enhance the tool's capabilities for smarter
proof searches and more robust conjecturing. While its primary target
is Isabelle-novices without extensive library support, insights,
feedback, and feature suggestions from seasoned users are highly
valued and appreciated.
Warm regards,
Yutaka
Email Gateway (Sep 01 2023 at 10:16):From: Lawrence Paulson <lp15@cam.ac.uk>
That certainly looks cool! Is there a paper?
Larry Paulson
Last updated: Jan 04 2025 at 20:18 UTC