# Abduction Prover in Isabelle/HOL

arXiv: https://arxiv.org/abs/2606.04877 · HTML: https://mlsanity.com/paper/2606.04877/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 6 references that are in the map.
- First posted on arXiv 3 Jun 2026.

## Builds on (most cited first, 2 of 2)

- [A Proof Strategy Language and Proof Script Generation for Isabelle/HOL](https://mlsanity.com/paper/1606.02941/) (2016)
- [Goal-Oriented Conjecturing for Isabelle/HOL](https://mlsanity.com/paper/1806.04774/) (2018)

## Abstract (arXiv)

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.