发表机构
Université Paris-Saclay; ENS Paris-Saclay; University of Greifswald（巴黎萨克雷大学; 巴黎萨克雷高等师范学院; 格赖夫斯瓦尔德大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种在Dedukti框架中验证高阶逻辑自动定理证明器证明的通用方法论，应用于EP演算并集成至Leo-III，实现约80%证明步骤自动重构，成为首个支持独立可检查证明重构的高阶证明器。
AI 中文摘要
我们识别了在Dedukti逻辑框架中验证自动定理证明器证明的常见挑战和要求，并开发了一种通用方法论，用于推导演算规则和证明步骤（包括子句化）的编码。然后，我们将此方法论应用于高阶逻辑的EP演算，并将其集成到自动定理证明器Leo-III中。由此产生的原型自动重构了约80%的生成的证明步骤，使Leo-III成为首个支持独立可检查证明重构的高阶自动定理证明器，并为跨系统重用提供了基础。该实现还发现了Leo-III中的几个错误。
英文摘要
We identify common challenges and requirements for verifying proofs from automated theorem provers in the Dedukti logical framework and develop a general methodology for deriving encodings of calculus rules and proof steps, including clausification. We then apply this methodology to the EP calculus for higher-order logic and integrate it into the automated theorem prover Leo-III. The resulting prototype reconstructs about 80% of generated proof steps automatically, making Leo-III the first higher-order automated theorem prover to support independently checkable proof reconstruction and providing a basis for cross-system reuse. The implementation uncovered several bugs in Leo-III.
Journal refLPAR-26 - 26th Conference on Logic for Programming, Artificial intelligence, and Reasoning, Oct 2026, Spetses Island, Greece
