Research
Abduction Prover in Isabelle/HOL
arXiv:2606.04877v1 Announce Type: cross Abstract: Proof assistants based on expressive logics suffer limited automation for proof search, raising the cost of formal verification based on proof assista
arXiv:2606.04877v1 Announce Type: cross Abstract: Proof assistants based on expressive logics suffer limited automation for proof search, raising the cost of formal verification based on proof assistants. We address this problem by introducing the Abduction Prover for Isabelle/HOL. Given a challenging proof goal, the Abduction Prover constructs a proof script for the goal by identifying useful conjectures using abductive reasoning.
Source: arXiv cs.AI | 2026-06-04