Automated Theorem Proving in Euler Diagram Systems
Automated Theorem Proving in Euler Diagram Systems
复制标题
欧拉图系统中的自动定理证明
DOI：
10.1007/s10817-007-9069-y
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
J. Southern
中科院分区：
文献类型：
--
作者：
Gem Stapleton;Judith Masthoff;Jean Flower;A. Fish;J. Southern
图解推理在许多应用领域中具有重要的潜力。本文重点介绍了简单但广泛使用的欧拉图，它构成了许多更具表现力的逻辑的基础。我们已经实现了一个图形定理证明，称为伊迪丝，它可以访问四个声音和完整的欧拉图推理规则集。此外，对于每一个规则集，我们开发了一个复杂的启发式来指导搜索的证明。本文是关于理解推理规则集的选择如何影响寻找证明所需的时间。这种理解将影响其他逻辑推理规则的设计。此外，这项工作具体到欧拉图直接受益于许多逻辑的基础上欧拉图。我们研究如何找到一个证明所需的时间不仅取决于证明任务，但也对推理系统使用。我们的评估使我们能够预测推理系统的最佳选择，给定一个证明任务，在所需的时间方面，我们提取了一个指南，用于定义其他逻辑的推理规则，以尽量减少时间要求。
Diagrammatic reasoning has the potential to be important in numerous application areas. This paper focuses on the simple, but widely used, Euler diagrams that form the basis of many more expressive logics. We have implemented a diagrammatic theorem prover, called Edith, which has access to four sound and complete sets of reasoning rules for Euler diagrams. Furthermore, for each rule set we develop a sophisticated heuristic to guide the search for a proof. This paper is about understanding how the choice of reasoning rule set affects the time taken to find proofs. Such an understanding will influence reasoning rule design in other logics. Moreover, this work specific to Euler diagrams directly benefits the many logics based on Euler diagrams. We investigate how the time taken to find a proof depends not only on the proof task but also on the reasoning system used. Our evaluation allows us to predict the best choice of reasoning system, given a proof task, in terms of time taken, and we extract a guide for defining reasoning rules for other logics in order to minimize time requirements.