nach oben

Journal of Logic, Language and Information

Erschienen in:

01.12.2015

Speedith: A Reasoner for Spider Diagrams

Erschienen in: Journal of Logic, Language and Information | Ausgabe 4/2015

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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 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.

Vorheriger Artikel Set Venn Diagrams Applied to Inclusions and Non-inclusions

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

The use of diagrams as evidence, or as a tool for constructing proofs, predates modern efforts of formalisation of logic. An early example of the use of diagrams in proofs is Euclid’s Elements. In the past, diagrams were used in the context of geometry, or geometrical representations of concepts from algebra, number theory, analysis, topology and category theory.

We first introduced Speedith in Urbas et al. (2012). This paper gives a comprehensive account of Speedith, its design and theoretical properties, and also its further developments regarding the selection of inference rules, hand-drawing interface and pluggable infrastructure.

The system in Howse et al. (2005) is a proper fragment of that implemented in Speedith and was proved complete in the absence of \(\longrightarrow \), \(\longleftrightarrow \) and \(\lnot \). We enlarge the set of inference rules to obtain completeness in this syntactically richer logic.

Note that we use labels on spider feet in order to be able to refer to specific spiders. However, as can be observed from the definition of spiders above, these labels do not form part of the syntax of spider diagrams. They are a convenience, and can be arbitrarily and freshly chosen every time an inference rule is applied on a diagram. This means that, for example, two drawn spider diagrams that are identical apart from the spider labels have the same syntax.

A spider with an empty habitat is a contradiction, as it would imply that there exists an element that does not belong to any set.

So, each zone \(( in , out )\) in Z ensures that \( in \cup out =L\).

Introducing a contour in abstract syntax is straightforward. However, drawing an additional contour may be more complex, for example, it may not be drawable as a single circle. We use iCircle algorithm for laying out spider diagrams—for details, see Sect. 4.4.2.

In Speedith, \(\bot \) is equivalently represented by \(\lnot \top \).

Note that we assume an empty disjunction is \(\perp \).

This rule has been added in Urbas et al. (2012) and is not part of the original specification of spider diagrams in Howse et al. (2005).

Regions in two unitary spider diagrams that represent the same set are called corresponding regions. Corresponding regions can be identified syntactically and are therefore suitable as a proof-theoretic tool for defining inference rules. This was first seen in Howse et al. (2002), where that work is generalized in “Appendix 1” so that corresponding regions can be used for the formalization of inference rules.

iCircles was originally created by Stapleton et al. (2012) to draw Euler diagrams (spider diagrams without any spiders in them). Flower then extended iCircles to include the visualisation of spiders, so iCircles supports the visualisation of unitary spider diagrams only, but not compound spider diagrams.

An empty unitary spider diagram is the tuple \(d = (\emptyset , \{(\emptyset , \emptyset )\}, \emptyset , \emptyset , \emptyset )\).

Hand-drawn input support for spider diagrams similar to SpiderDrawer is currently being developed by Wang et al. (2011) within the SketchSet tool. But unlike SpiderDrawer and Speedith, SketchSet is platform dependent and requires proprietary Windows libraries. Since this would seriously limit Speedith’s reach to users, we instead developed SpiderDrawer.

https://code.google.com/p/tessaract-ocr/.

Embedding SpiderDrawer’s canvas directly within Speedith’s proof panel (rather than using it as a separate pop-up window) is work that we plan for the future.

Bachmair, L., Ganzinger, H., & Waldmann, U. (1992). Set constraints are the monadic class

Bashford-Chuchla, C.T. (2014). Pen input interface for a diagrammatic theorem prover. Mphil dissertation, University of Cambridge Computer Laboratory, Cambridge, UK

Chang, S. H., Blagojevic, R., & Plimmer, B. (2012). Rata.gesture: A gesture recognizer developed using data mining. Artificial Ingelligence for Engineering Design, Analysis and Manufacturing, 26(3), 351–366.CrossRef

Damm, C., Hansen, K., & Thomsen, M. (2000) Tool support for cooperative object-oriented design: Gesture based modelling on an electronic whiteboard. In SIGCHI conference on human factors in computing systems, pp. 518–525. ACM, New York.

Dau, F. (2007). Constants and functions in peirce’s existential graphs. In ICCS, LNCS, Vol. 4604, pp. 429–442. Springer, Berlin.

De Chiara, R., Hammar, M., & Scarano, V. (2005). A system for virtual directories using euler diagrams. Electronic Notes in Theoretical Computer Science, 134, 33–53.CrossRef

Flower, J., Masthoff, J., & Stapleton, G. (2004). Generating readable proofs: A heuristic approach to theorem proving with spider diagrams. In A. Blackwell, K. Marriott, A. Shimojima (Eds.), Diagrammatic representation and inference. Lecture notes in computer science (Vol. 2980, pp. 166–181). New York, Springer. doi:10.1007/978-3-540-25931-2_17.

Gordon, M. J., Milner, A. J., & Wadsworth, C. P. (1979). Edinburgh LCF: A mechanised logic of computation. Lecture Notes in Computer Science (Vol. 78). New York: Springer. doi:10.1007/3-540-09724-4.

Hammer, E. (1995). Logic and visual information. CSLI.

Hammond, T., & Davis, R. (2002) Tahuti: A geometrical sketch recognition system for UML class diagrams. In AAAI spring symposium on sketch understanding.

Howse, J., Stapleton, G., Flower, J., & Taylor, J. (2002) Corresponding regions in Euler diagrams. In Diagrams. lecture notes in computer science, Vol. 2317, pp. 76–90. New York: Springer.

Howse, J., Stapleton, G., & Taylor, J. (2005). Spider diagrams. Journal of Computation and Mathematics, 8, 145–194.

Jamnik, M., Bundy, A., & Green, I. (1999). On automating diagrammatic proofs of arithmetic arguments. Journal of Logic, Language and Information, 8(3), 297–321.CrossRef

Jiang, Y., Tian, F., Zhang, X. L., Dai, G., & Wang, H. (2011). Understanding, manipulating and searching hand-drawn concept maps. ACM Transactions on Intelligent Systems and Technology, 3(11), 21.

Kent, S. (1997). Constraint diagrams: Visualizing invariants in object oriented modelling. In OOPSLA, SIGPLAN, Vol. 32, pp. 327–341. New York: ACM.

Keslter, H., Muller, A., Kraus, J., Buchholz, M., Gress, T., Kane, D., et al. (2008). Vennmaster: Area-proportional Euler diagrams for functional go analysis of microarrays. BMC Bioinformatics, 9(67).

Kortenkamp, U., & Richter-Gebert, J. (2004). Using automatic theorem proving to improve the usability of geometry software. In Procedings of the mathematical user-interfaces workshop, pp. 1–12.

Plimmer, B., & Freeman, I. (2007) A toolkit approach to sketched diagram recognition. In HCI, pp. 205–213. British Computer Society

Plimmer, B., Purchase, H., & Yang, H. (2010). SketchNode: Intelligent sketching support and formal diagramming. In OZCHI 2010, pp. 136–143. ACM.

Shin, S. J. (2009). The logical status of diagrams. Cambridge: Cambridge University Press.

Smith, R. (2007). An overview of the Tesseract OCR engine. In Proceedings of the ninth international conference on document analysis and recognition (ICDAR ’07), pp. 629–633. IEEE Computer Society.

Stapleton, G., Flower, J., Rodgers, P., & Howse, J. (2012). Automatically drawing Euler diagrams with circles. Journal of Visual Languages and Computing, 23(3), 163–193.CrossRef

Stapleton, G., Howse, J., Taylor, J., & Thompson, S. (2004). The expressiveness of spider diagrams. Journal of Logic and Computation, 14(6), 857–880.CrossRef

Stapleton, G., & Masthoff, J. (2007). Incorporating negation into visual logics: A case study using Euler diagrams. In Visual languages and computing 2007, pp. 187–194. Knowledge Systems Institute.

Stapleton, G., Masthoff, J., Flower, J., Fish, A., & Southern, J. (2007). Automated theorem proving in Euler diagram systems. Journal of Automated Reasoning, 39(4), 431–470.CrossRef

Stapleton, G., Plimmer, B., Delaney, A. & Rodgers, P. (2014). Combining sketching and traditional diagram editing tools. ACM Transactions on Intelligent Systems and Technology.

Stapleton, G., Taylor, J., Howse, J., & Thompson, S. (2009). The expressiveness of spider diagrams augmented with constants. Journal of Visual Languages and Computing, 20, 30–49.CrossRef

Swoboda, N., & Allwein, G. (2005). Heterogeneous reasoning with Euler/Venn diagrams containing named constants and FOL. In Proceedings of Euler diagrams 2004. ENTCS, Vol. 134. Elsevier.

Takemura, R. (2013). Proof theory for reasoning with Euler diagrams: A logic translation and normalization. Studia Logica, 101(1), 157–191.CrossRef

Tarski, A. (1944). The semantic conception of truth: And the foundations of semantics. Philosophy and Phenomenological Research, 4(3), 341–376.CrossRef

Urbas, M., & Jamnik, M. (2012). Diabelli: A heterogeneous proof system. In Proceedings of the international joint conference on automated reasoning. Lecture notes in computer science, Vol. 7364, pp. 559–566. New York: Springer.

Urbas, M., & Jamnik, M. (2014). A framework for heterogeneous reasoning in formal and informal domains. In T. Dwyer, H. Purchase, & A. Delaney (Eds.), Diagrams. Lecture notes in computer science, Vol. 8578, pp. 277–292. New York: Springer.

Urbas, M., Jamnik, M., Stapleton, G., & Flower, J. (2012). Speedith: A diagrammatic reasoner for spider diagrams. In Diagrams. Lecture notes in computer science, Vol. 7352, pp. 163–177. New York: Springer.

Wang, M., Plimmer, B., Schmieder, P., Stapleton, G., Rodgers, P., & Delaney, A. (2011). SketchSet: Creating Euler diagrams using pen or mouse. In IEEE symposium on visual languages and human-centric computing, Vol. 6898, pp. 75–82. IEEE Computer Society.

Winterstein, D., Bundy, A., & Gurr, C. (2004). Dr. Doodle: A diagrammatic theorem prover. In Proceedings of the international joint conference on automated reasoning. Lecture notes in artificial intelligence, Vol. 3097, pp. 331–335.

Titel: Speedith: A Reasoner for Spider Diagrams
Publikationsdatum: 01.12.2015
Erschienen in: Journal of Logic, Language and Information / Ausgabe 4/2015
Print ISSN: 0925-8531
Elektronische ISSN: 1572-9583
DOI: https://doi.org/10.1007/s10849-015-9229-0

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 4/2015

How Diagrams Can Support Syllogistic Reasoning: An Experimental Study

Set Venn Diagrams Applied to Inclusions and Non-inclusions

On the Diagrammatic Representation of Existential Statements with Venn Diagrams

Special issue on Euler and Venn Diagrams: Guest Editors’ introduction

Drawing Interactive Euler Diagrams from Region Connection Calculus Specifications