Speedith: A Reasoner for Spider Diagrams
Tóm tắt
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.
Tài liệu tham khảo
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.
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.
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.
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.
Stapleton, G., Howse, J., Taylor, J., & Thompson, S. (2004). The expressiveness of spider diagrams. Journal of Logic and Computation, 14(6), 857–880.
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.
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.
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.
Tarski, A. (1944). The semantic conception of truth: And the foundations of semantics. Philosophy and Phenomenological Research, 4(3), 341–376.
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.
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 computing, pp. 75–82. IEEE.
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.