arXiv:2606.04877cs.LOcs.AI2026-06中稿 · Isabelle2026
用反演推理自动发现证明所需假设，提升Isabelle/HOL的自动化水平。
Abduction Prover in Isabelle/HOL
- 基于反演推理挖掘有助于证明目标的有用猜想
- 可生成完整证明脚本，解决复杂目标验证难题
- 适合需要高效形式化验证的研究者使用
基于高表达力逻辑的证明助手在证明搜索自动化方面存在局限，增加了基于证明助手的形式化验证成本。本文提出Isabelle/HOL的反演证明器（Abduction Prover）。面对复杂证明目标时，该工具通过反演推理识别出有用的猜想，并据此构建完整的证明脚本。
原文摘要 · Abstract (English)
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.
形式化验证证明助手反演推理
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。