System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level
System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level
复制标题
系统描述：TRAMP：在断言级别将机器发现的证明转换为 ND 证明
DOI：
10.1007/10721959_37
复制
发表时间：
2000
影响因子：
10.4
通讯作者：
A. Meier
中科院分区：
文献类型：
--
作者：
A. Meier
Tramp系统将一阶逻辑的几个自动定理证明器的输出与等式转换为断言级别的自然演绎证明。通过这个接口，其他系统，如证明呈现系统或交互式演绎系统，可以访问最初由Tramp接口的任何系统生成的证明，只需根据自己的需要调整断言级证明。
The Tramp system transforms the output of several automated theorem provers for first order logic with equality into natural deduction proofs at the assertion level. Through this interface, other systems such as proof presentation systems or interactive deduction systems can access proofs originally produced by any system interfaced by Tramp only by adapting the assertion level proofs to their own needs.