arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2104.13645cs.AIcs.LO
收藏

Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)

Technical University Darmstadt(达姆施塔特工业大学)

Christoph Wernhard, Wolfgang Bibel

英文摘要:

The material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features in selected problems and their proofs which offer the potential of guiding proof search in a more direct way. The studied problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)". The features include the well-known concept of lemmas. For their elaboration both human and automated proofs of selected theorems are taken into a close comparative consideration. The study at the same time accounts for a coherent and comprehensive formal reconstruction of historical work by Łukasiewicz, Meredith and others. First experiments resulting from the study indicate novel ways of lemma generation to supplement automated first-order provers of various families, strengthening in particular their ability to find short proofs.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑