{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T08:52:49Z","timestamp":1775638369496,"version":"3.50.1"},"reference-count":45,"publisher":"Wiley","license":[{"start":{"date-parts":[[2010,2,1]],"date-time":"2010-02-01T00:00:00Z","timestamp":1264982400000},"content-version":"unspecified","delay-in-days":1857,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["LMS J. Comput. Math."],"published-print":{"date-parts":[[2005]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The use of diagrams in mathematics has traditionally been restricted to guiding intuition and communication. With rare exceptions such as Peirce's alpha and beta systems, purely diagrammatic formal reasoning has not been in the mathematician's or logician's toolkit. This paper develops a purely diagrammatic reasoning system of \u201cspider diagrams\u201d that builds on Euler, Venn and Peirce diagrams. The system is known to be expressively equivalent to first-order monadic logic with equality. Two levels of diagrammatic syntax have been developed: an \u2018abstract\u2019 syntax that captures the structure of diagrams, and a \u2018concrete\u2019 syntax that captures topological properties of drawn diagrams. A number of simple diagrammatic transformation rules are given, and the resulting reasoning system is shown to be sound and complete.<\/jats:p>","DOI":"10.1112\/s1461157000000942","type":"journal-article","created":{"date-parts":[[2013,8,6]],"date-time":"2013-08-06T11:42:44Z","timestamp":1375789364000},"page":"145-194","source":"Crossref","is-referenced-by-count":82,"title":["Spider Diagrams"],"prefix":"10.1112","volume":"8","author":[{"given":"John","family":"Howse","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gem","family":"Stapleton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Taylor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2010,2,1]]},"reference":[{"key":"S1461157000000942_ref013","first-page":"166","article-title":"\u2018Generating readable proofs: a heuristic approach to theorem proving with spider diagrams\u2019","author":"Flower","year":"2004","journal-title":"Proc. Diagrams"},{"key":"S1461157000000942_ref030","unstructured":"30 Lull R. , Ars magma (Lyons, 1517)."},{"key":"S1461157000000942_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/j.jvlc.2005.03.001"},{"key":"S1461157000000942_ref018","first-page":"72","volume-title":"\u2018Towards a formalization of constraint diagrams\u2019","author":"Gil","year":"2001"},{"key":"S1461157000000942_ref004","first-page":"260","article-title":"\u2018Computing reading trees for constraint diagrams\u2019","author":"Fish","year":"2003","journal-title":"Proc. AGTIVE"},{"key":"S1461157000000942_ref025","first-page":"127","volume-title":"\u2018A sound and complete diagrammatic reasoning system\u2019","author":"Howse","year":"2000"},{"key":"S1461157000000942_ref038","unstructured":"38 Stapleton G. , \u2018Reasoning with constraint diagrams\u2019, PhD Thesis, University of Brighton, August (2004)."},{"key":"S1461157000000942_ref015","first-page":"272","volume-title":"\u2018Layout metrics for Euler diagrams\u2019","author":"Flower","year":"2003"},{"key":"S1461157000000942_ref022","unstructured":"22 Howse J. , Molina F. , Shin S.-J. and Taylor J. , \u2018On diagram tokens and types\u2019, Proc. Diagrams (2002) (International Conference on the Theory and Application of Diagrams), Lecture Notes in Artificial Intelligence 2317 (Springer, 2002) 76\u201390."},{"key":"S1461157000000942_ref029","first-page":"47","volume-title":"\u2018Comparing the efficacy of visual languages\u2019","author":"LEMON","year":"2002"},{"key":"S1461157000000942_ref043","doi-asserted-by":"publisher","DOI":"10.1080\/14786448008626877"},{"key":"S1461157000000942_ref003","first-page":"53","article-title":"\u2018Investigating reasoning with constraint diagrams\u2018","author":"Fish","year":"2004","journal-title":"Proc. Visual Languages and Formal Methods"},{"key":"S1461157000000942_ref037","volume-title":"The logical status of diagrams","author":"Shin","year":"1994"},{"key":"S1461157000000942_ref036","unstructured":"36 Luzio P. Scotto Di , \u2018Patching up a logic of Venn diagrams\u2019, Proc. 6th CSLI Workshop on Logic, Language and Computation (CSLI Publications, Stanford, 2000)."},{"key":"S1461157000000942_ref014","first-page":"279","article-title":"\u2018Generating proofs with spider diagrams using heuristics\u2019","author":"Flower","year":"2004","journal-title":"Proc. VLC"},{"key":"S1461157000000942_ref012","first-page":"71","volume-title":"Proc. HCC","author":"Flower","year":"2002"},{"key":"S1461157000000942_ref001","unstructured":"1 Dreban B. ,and Goldfarb D , The decision problem. Solvable classes of quantificational formulas (Addison Wesley, 1979)."},{"key":"S1461157000000942_ref010","first-page":"116","article-title":"\u2018Automated theorem proving with spider diagrams\u2019","author":"Flower","year":"2004","journal-title":"Proc. CATS"},{"key":"S1461157000000942_ref002","unstructured":"2 Euler L. , Lettres a une princesse d\u2018Allemagne sur divers sujets de physique et de philosophie, vol. 2 (1761) Letters 102\u2013108."},{"key":"S1461157000000942_ref039","first-page":"263","article-title":"\u2018A constraint diagram reasoning system\u2019","author":"Stapleton","year":"2003","journal-title":"Proc. VLC"},{"key":"S1461157000000942_ref005","first-page":"51","article-title":"\u2018Towards a default reading for constraint diagrams\u2019","author":"Fish","year":"2004","journal-title":"Proc. Diagrams"},{"key":"S1461157000000942_ref006","first-page":"161","volume-title":"\u2018A reading algorithm for constraint diagrams\u2019","author":"Fish","year":"2003"},{"key":"S1461157000000942_ref042","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/14.6.857"},{"key":"S1461157000000942_ref044","first-page":"128","volume-title":"\u2018Ensuring the drawability of extended Euler diagrams for up to 8 sets\u2019","author":"Verroust","year":"2004"},{"key":"S1461157000000942_ref009","first-page":"61","article-title":"\u2018Generating Euler diagrams\u2019","author":"Flower","year":"2002","journal-title":"Proc. Diagrams"},{"key":"S1461157000000942_ref011","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-003-0036-8"},{"key":"S1461157000000942_ref016","first-page":"453","volume-title":"\u2018Constraint diagrams: a step beyond UML\u2019","author":"Gil","year":"1999"},{"key":"S1461157000000942_ref020","first-page":"235","volume-title":"\u2018On visual formalisms\u2019","author":"Harel","year":"1998"},{"key":"S1461157000000942_ref021","first-page":"174","volume-title":"\u2018Type-syntax and token-syntax in diagrammatic systems\u2019","author":"Howse","year":"2001"},{"key":"S1461157000000942_ref019","volume-title":"Logic and visual information","author":"Hammer","year":"1995"},{"key":"S1461157000000942_ref023","first-page":"402","volume-title":"\u2018SD2: a sound and complete diagrammatic reasoning system\u2019","author":"Howse","year":"2000"},{"key":"S1461157000000942_ref017","first-page":"130","volume-title":"\u2018Formalising spider diagrams\u2019","author":"Gil","year":"1999"},{"key":"S1461157000000942_ref024","first-page":"26","article-title":"\u2018On the completeness and expressiveness of spider diagram systems\u2019","author":"Howse","year":"2000","journal-title":"Proc. Diagrams"},{"key":"S1461157000000942_ref026","first-page":"138","volume-title":"\u2018Reasoning with spider diagrams\u2019","author":"Howse","year":"1999"},{"key":"S1461157000000942_ref027","doi-asserted-by":"publisher","DOI":"10.1006\/jvlc.2000.0210"},{"key":"S1461157000000942_ref028","doi-asserted-by":"publisher","DOI":"10.1145\/263700.263756"},{"key":"S1461157000000942_ref035","first-page":"147","volume-title":"\u2018Dynamic Euler diagram drawing\u2019","author":"Rodgers","year":"2004"},{"key":"S1461157000000942_ref031","unstructured":"31 Molina F. , \u2018Reasoning with extended Venn-Peirce diagrammatic systems\u2019, PhD Thesis, University of Brighton, (2001)."},{"key":"S1461157000000942_ref008","doi-asserted-by":"crossref","unstructured":"8 Fitting M. , First order logic and automated theorem proving (Springer, 1996).","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"S1461157000000942_ref032","first-page":"66","volume-title":"\u2018Drawing graphs in Euler Diagrams\u2019","author":"Mutton","year":"2004"},{"key":"S1461157000000942_ref033","unstructured":"33 OBJECT MANAGEMENT GROUP,\u2018Unified Modeling Language specification\u2019, availableatwww.omg.org."},{"key":"S1461157000000942_ref034","volume-title":"Collected papers","author":"Peirce","year":"1933"},{"key":"S1461157000000942_ref040","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exi041"},{"key":"S1461157000000942_ref041","first-page":"112","volume-title":"What can spider diagrams say?\u2019","author":"Stapledon","year":"2004"},{"key":"S1461157000000942_ref045","unstructured":"45 Warmer J. and Kleppe A. , The Object Constraint Language: precise modeling with UML (Addison-Wesley, 1998)."}],"container-title":["LMS Journal of Computation and Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1461157000000942","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T02:28:46Z","timestamp":1559874526000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1461157000000942\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"references-count":45,"alternative-id":["S1461157000000942"],"URL":"https:\/\/doi.org\/10.1112\/s1461157000000942","relation":{},"ISSN":["1461-1570"],"issn-type":[{"value":"1461-1570","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}