Kevin Kappelmann renamed stream new projects to New Members & Projects.
Kevin Kappelmann changed the access permissions for this stream from Public to Web-public.
Hi there,
I am Yutaka.
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 selected 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
Last updated: Dec 03 2024 at 16:25 UTC