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.

翻译：基于表达力丰富逻辑的证明助手在证明搜索方面自动化程度有限，这增加了基于证明助手的形式化验证成本。我们通过引入Isabelle/HOL的溯因证明器来解决这一问题。给定一个具有挑战性的证明目标，该溯因证明器通过溯因推理识别有用猜想，为目标构建证明脚本。