Speedith swMATH ID: 19455 Software Authors: Urbas, M., Jamnik, M., Stapleton, G., Flower, J. Description: Speedith - a diagrammatic reasoner for spider diagrams. In this paper, we introduce Speedith which is a diagrammatic theorem prover for the language of spider diagrams. Spider diagrams are a well-known logic for which there is a sound and complete set of inference rules. Speedith provides a way to input diagrams, transform them via the diagrammatic inference rules, and prove diagrammatic theorems. It is designed as a program that plugs into existing general purpose theorem provers. This allows for seamless formal verification of diagrammatic proof steps within established proof assistants such as Isabelle. 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. Homepage: http://link.springer.com/chapter/10.1007/978-3-642-31223-6_19 Related Software: Diabelli; Openproof; HOL; Isabelle; VAMPIRE; Dr.Doodle; MaSh; Hets; HOL Light; WordNet; Isabelle/HOL; Octave; ACL2; VOWL; SOVA; Protege; Tesseract; SketchNode; Tahuti; SketchSet Cited in: 5 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Speedith: a reasoner for spider diagrams. Zbl 1362.68252Urbas, Matej; Jamnik, Mateja; Stapleton, Gem 2015 all top 5 Cited by 12 Authors 4 Jamnik, Mateja 2 Stapleton, Gem 2 Urbas, Matej 1 Cheng, Peter C.-H. 1 Demey, Lorenz 1 Garcia Garcia, Grecia 1 Raggi, Daniel 1 Sato, Yuri 1 Shams, Zohreh 1 Smessaert, Hans 1 Stockdill, Aaron 1 Sutherland, Holly E. A. Cited in 2 Serials 1 Journal of Logic, Language and Information 1 Annals of Mathematics and Artificial Intelligence Cited in 4 Fields 5 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Geometry (51-XX) 1 Convex and discrete geometry (52-XX) Citations by Year