凡人的身份证明
Proof identity for mere mortals
摘要：
证明恒等式问题：什么时候两个证明是相同的？当人们反思数学实践时，这个问题自然会出现。这个问题可以理解为对数理逻辑的挑战，事实上，在证明论文献中可以找到关于这个问题的各种观点。从证明理论的角度来看，挑战是通过制定新的演算，消除“官僚主义”;技术，如规范化和削减消除，以及证明压缩，被采用。在这份说明中，一个新的角度对证明身份的问题进行了概述。新的方法采用的概念和自动定理证明的工具，并补充了来自纯证明理论的理论观点。实际的方法说明了来自TPTP问题库的实验。
英文摘要：
The proof identity problem asks: When are two proofs the same? The question naturally occurs when one reflects on mathematical practice. The problem understandably can be seen as a challenge for mathematical logic, and indeed various perspectives on the problem can be found in the proof theory literature. From the proof theory perspective, the challenge is met by laying down new calculi that eliminate ``bureaucracy''; techniques such as normalization and cut-elimination, as well as proof compression, are employed. In this note a new perspective on the proof identity problem is outlined. The new approach employs the concepts and tools of automated theorem proving and complements the rather more theoretical perspectives coming from pure proof theory. The practical approach is illustrated with experiments coming from the TPTP Problem Library.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
