Kevin Kappelmann renamed stream new projects to New Members & Projects.
Kevin Kappelmann changed the access permissions for this stream from Public to Web-public.
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:
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.
Last updated: Dec 07 2023 at 16:21 UTC