AI 中文总结
探讨证明理论与依赖类型理论在设计证明助手中的基础差异，提出六个证明理论视角更优的主题，借助Abella定理证明器展示自然内涵式方法，为语言和逻辑元理论推理提供优雅环境。
AI 中文摘要
本文探讨了交互式定理证明器设计中证明理论与依赖类型理论（DTT）之间的基础差异。尽管多个已实现系统使用依赖类型λ演算来表示证明，但尚无主要证明助手基于现代结构化证明理论设计，而相继式演算提供了有吸引力的替代框架。提出六个证明理论视角优于DTT视角的具体主题，包括逻辑与证明结构分离等。通过Abella定理证明器展示了一种自然、内涵式方法，它利用λ树语法和nabla量词为涉及复杂绑定的语言和逻辑元理论推理提供优雅环境。
英文摘要
This paper examines the foundational distinctions between proof theory and dependent type theory (DTT) in the design of interactive theorem provers. While several implemented systems are designed using the dependently typed λ-calculus to represent proofs, no major proof assistant is designed using modern structural proof theory, even though, as I will argue here, the sequent calculus offers a compelling alternative framework. Six specific topics are proposed where the proof-theoretic perspective is arguably superior to the DTT perspective. These topics include the separation of logic from proof structure, the strategic use of non-determinism in proof reconstruction, and the avoidance of complex typing-discipline issues such as universe levels and proof irrelevance. The final topic -- the treatment of bindings -- is further developed to demonstrate how a natural, intensional approach is achieved through the mobility of binders. This methodology is illustrated via the Abella theorem prover, which leverages lambda-tree syntax and the nabla-quantifier to provide an elegant environment for reasoning about the meta-theory of languages and logics involving complex binding.
CommentsIn Proceedings LFMTP 2026, arXiv:2607.10318
Journal refEPTCS 448, 2026, pp. 18-28
