EKSTRAKTO：从 TSTP 文件重建 Dedukti 证明的工具（扩展摘要）

证明助手常调用自动定理证明器来证明子目标。然而，每个证明器有其自身的证明演算，且其产生的证明迹常缺乏构建完整证明的诸多细节。因此这些迹难以在证明助手中检查与复用。Dedukti 是一个证明检查器，其证明可翻译至多种证明助手：Coq、HOL、Lean、Matita、PVS。我们实现了一个工具，从 TSTP 文件中提取 TPTP 子问题，并利用能生成 Dedukti 证明的自动证明器（如 ZenonModulo 或 ArchSAT）在 Dedukti 中重建完整证明。该工具是通用的：它不对产生迹的证明器的证明演算作任何假设，且可使用不同证明器来生成 Dedukti 证明。我们将工具应用于自动定理证明器在 TPTP 库的 CNF 问题上产生的迹，能够为其中很大一部分重建证明，显著增加了可为这些问题获得的 Dedukti 证明数量。