Tipi：一个基于TPTP的理论开发环境，强调证据分析
Tipi: A TPTP-based theory development environment emphasizing proof analysis
摘要：
在一些理论开发任务中，一旦证明一个定理（猜想）可以从背景理论（前提）推导出来，问题就得到了满意的解决。根据一个人的动机，从前提推导猜想的细节可能重要，也可能不重要。然而，在某些情况下，人们希望从理论发展中得到更多，而不仅仅是从背景理论中推导出目标定理。人们可能想知道在自动定理证明器输出的证明过程中使用了背景理论的哪些前提（当证明可用时），它们在适当的意义上是否都是必要的（以及为什么），是否可以找到替代证明，等等。那么，问题是在理论发展中支持证据分析;本文描述的工具Tipi旨在提供准确的证据分析。
英文摘要：
In some theory development tasks, a problem is satisfactorily solved once it is shown that a theorem (conjecture) is derivable from the background theory (premises). Depending on one's motivations, the details of the derivation of the conjecture from the premises may or may not be important. In some contexts, though, one wants more from theory development than simply derivability of the target theorems from the background theory. One may want to know which premises of the background theory were used in the course of a proof output by an automated theorem prover (when a proof is available), whether they are all, in suitable senses, necessary (and why), whether alternative proofs can be found, and so forth. The problem, then, is to support proof analysis in theory development; the tool described in this paper, Tipi, aims to provide precisely that.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
