Generating Readable Proofs: A Heuristic Approach to Theorem Proving With Spider Diagrams
Generating Readable Proofs: A Heuristic Approach to Theorem Proving With Spider Diagrams
复制标题
生成可读的证明：用蜘蛛图证明定理的启发式方法
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Gem Stapleton
中科院分区：
文献类型：
--
作者：
Jean Flower;Judith Masthoff;Gem Stapleton
图解推理的一个重要目的是使人们更容易创造和理解逻辑论证。我们已经在蜘蛛图上工作过，它直观地表达了逻辑语句。理想情况下，自动生成的证明应该简短易懂。现有的蜘蛛图证明生成器可以成功地编写证明，但它们可能很长而且很笨拙。在本文中，我们提出了一种新的方法证明写作的图表系统，这是保证找到最短的证明，并可以扩展到其他可读性标准。我们应用A * 算法，并开发了一个可接受的启发式函数来指导自动证明构造。我们证明了所使用的启发式的有效性。这项工作已被实施的蜘蛛图推理工具的一部分。
An important aim of diagrammatic reasoning is to make it easier for people to create and understand logical arguments. We have worked on spider diagrams, which visually express logical statements. Ideally, automatically generated proofs should be short and easy to understand. An existing proof generator for spider diagrams successfully writes proofs, but they can be long and unwieldy. In this paper, we present a new approach to proof writing in diagrammatic systems, which is guaranteed to find shortest proofs and can be extended to incorporate other readability criteria. We apply the A * algorithm and develop an admissible heuristic function to guide automatic proof construction. We demonstrate the effectiveness of the heuristic used. The work has been implemented as part of a spider diagram reasoning tool.