Abduction Prover in Isabelle/HOL
Yutaka Nagashima, Daniel Sebastian Goc
cs.LO cs.AI cs.PL cs.SE
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.
Topics
Classified with taxonomy v2 on Wed, 2 Sept 2026.