SC-TPTP：面向序数演算的TPTP导出格式扩展
计算机科学中的逻辑
2025-07-16 v1
摘要
为了实现证明在不同证明系统之间的迁移，特别是从一阶自动定理证明器(ATP)到交互式定理证明器(ITP)之间的迁移，我们指定了TPTP导出文本格式的一个扩展，用于描述一阶逻辑中的证明：SC-TPTP。为避免标准的不断扩散，我们提出的格式通过聚焦于序数形式来对TPTP导出格式进行过度指定。这样做可以提供高度细节、忠于数学传统，并覆盖多个现有工具，特别是基于表格的策略。我们利用这一格式，使Lisa交互式定理证明器能够查询Go\'eland自动定理证明器，并实现一组能够解析、打印和检查SC-TPTP证明、导出为Coq文件、并从高级证明步骤中重建低级证明步骤的工具库。
引用
@article{arxiv.2507.11349,
title = {SC-TPTP: An Extension of the TPTP Derivation Format for Sequent-Based Calculus},
author = {Julie Cailler and Simon Guilloud},
journal= {arXiv preprint arXiv:2507.11349},
year = {2025}
}