mlsanityData to 14 Oct 2026

Abduction Prover in Isabelle/HOL

arXiv 2606.04877 ↗First posted 3 Jun 2026cs.LO cs.AI cs.PLcited by 0

Not on the map. Why?

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.

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

2 of 6 references.

References · 2

  1. 2016A Proof Strategy Language and Proof Script Generation for Isabelle/HOLcited by 5
  2. 2018Goal-Oriented Conjecturing for Isabelle/HOLcited by 1

Built on by

Not cited yet.

Similar, not cited

Close in wording, no citation either way

  1. 2022Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
  2. 2025L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL ↗
  3. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
  4. 2024Abductive Reasoning in a Paraconsistent Framework
  5. 2025Complexity of Abduction in Lukasiewicz Logic ↗
  6. 2026Vibe Coding an LLM-powered Theorem Prover
  7. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoning
  8. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofs