会议论文详细信息
CICM Workshop on Empirically Successful Automated Reasoning in Mathematics
Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions
计算机科学;数学
Stefan Hetzl ; Alexander Leitsch ; Daniel Weller ; Bruno Woltzenlogel Paleo
Others  :  http://CEUR-WS.org/Vol-378/paper2.pdf
PID  :  46705
学科分类:计算机科学(综合)
来源: CEUR
PDF
【 摘 要 】

CERES, HLK and ProofTool form together a system for the computer-aided analysis of mathematical proofs. This analysis is based on a proof transformation known as cut-elimination, which corresponds to the elimination of lemmas in the corresponding informal proofs. Consequently, the resulting formal proof in atomic-cut normal form corresponds to a direct, i.e. without lemmas, informal mathematical proof of the given theorem. In this paper, we firstly describe the current status of the whole system from the point of view of its usage. Subsequently, we discuss each component in more detail, briefly explaining the formal calculi (LK and LKDe) used, the intermediary language HandyLK, the CERES method of cut-elimination by resolution and the extraction of Herbrand sequents. Three successful cases of application of the system to mathematical proofs are then summarized. And finally we discuss extensions of the system that are currently under development or that are planned for the short-term future.

【 预 览 】
附件列表
Files Size Format View
Proof Analysis with HLK, CERES and ProofTool: Current Status and Future Directions 449KB PDF download
  文献评价指标  
  下载次数:9次 浏览次数:8次