Speedith: A reasoner for spider diagrams

Matej Urbas, M. Jamnik, Gem Stapleton

Research output: Contribution to journalArticle

Abstract

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 exist-ing 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.
Original languageEnglish
Pages (from-to)487-540
Number of pages54
JournalJournal of Logic, Language and Information
Volume24
Issue number4
DOIs
Publication statusPublished - 1 Dec 2015

Bibliographical note

The final publication is available at Springer via http://dx.doi.org/10.1007/s10849-015-9229-0

Keywords

  • interactive theorem proving
  • diagrammatic reasoning
  • knowledge representation
  • automated reasoning

Fingerprint Dive into the research topics of 'Speedith: A reasoner for spider diagrams'. Together they form a unique fingerprint.

  • Cite this