Speedith: A Reasoner for Spider Diagrams
Speedith: A Reasoner for Spider Diagrams
复制标题
Speedith：蜘蛛图推理机
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Gem Stapleton
中科院分区：
文献类型：
--
作者：
Matej Urbas;M. Jamnik;Gem Stapleton
在本文中，我们介绍了Speedith这是一个交互式的图形定理证明著名的语言蜘蛛图。Speedith提供了一种输入蜘蛛图的方法，通过图解推理规则转换它们，并证明图解定理。Speedith的推理规则是健全和完整的，扩展了以前的研究，包括所有的经典逻辑连接词。除了作为一个独立的证明系统，Speedith还被设计为一个程序，插入到现有的通用定理证明器。这允许其他系统通过Speedith访问图解推理，以及在标准的图解证明助手中对图解证明步骤进行正式验证。我们描述了Speedith的一般结构，图形语言，自动机制，绘制的图表时，推理规则适用于他们，以及如何构建正式的图表证明。
In this paper, we introduce Speedith which is an interactive diagrammatic theorem prover for the well-known language of spider diagrams. Speedith provides a way to input spider diagrams, transform them via the diagrammatic inference rules, and prove diagrammatic theorems. Speedith’s inference rules are sound and complete, extending previous research by including all the classical logic connectives. In addition to being a stand-alone proof system, Speedith is also designed as a program that plugs into existing general purpose theorem provers. This allows for other systems to access diagrammatic reasoning via Speedith, as well as a formal verification of diagrammatic proof steps within standard sentential proof assistants. We describe the general structure of Speedith, the diagrammatic language, the automatic mechanism that draws the diagrams when inference rules are applied on them, and how formal diagrammatic proofs are constructed.
DOI：
10.1016/j.jvlc.2012.02.001
发表时间：
2012-06
期刊：
J. Vis. Lang. Comput.
影响因子：
--
作者：
Gem Stapleton;Jean Flower;P. Rodgers;J. Howse
通讯作者：
Gem Stapleton;Jean Flower;P. Rodgers;J. Howse