Abstract
Proof systems play a major role in the formal study of diagrammatic logical systems. Typically, the style of inference is not directly comparable to traditional sentential systems, to study the diagrammatic aspects of inference. In this work, we present a proof system for Euler diagrams with shading in the style of sequent calculus. We prove it to be sound and complete. Furthermore we outline how this system can be extended to incorporate heterogeneous logical descriptions. Finally, we explain how small changes allow for reasoning with intuitionistic logic.
This work was supported by EPSRC Research Programme EP/N007565/1 Science of Sensor Systems Software.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Compare with the textbook by Negri et al. [9].
- 2.
More precisely, these logics are typically defined by the lack of these rules.
References
Alves, S., Fernández, M., Mackie, I.: A new graphical calculus of proofs. In: Echahed, R. (ed.) TERMGRAPH 2011, vol. 48, pp. 69–84 (2011)
Barwise, J., Etchemendy, J.: Heterogeneous logic. In: Logical Reasoning with Diagrams, pp. 179–200. Oxford University Press Inc. (1996)
Burton, J., Stapleton, G., Howse, J.: Completeness proof strategies for Euler diagram logics. In: Euler Diagrams 2012, vol. 854, pp. 2–16. CEUR (2012)
de Freitas, R., Viana, P.: A graph calculus for proving intuitionistic relation algebraic equations. In: Cox, P., Plimmer, B., Rodgers, P. (eds.) Diagrams 2012. LNCS (LNAI), vol. 7352, pp. 324–326. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31223-6_40
Gentzen, G.: Untersuchungen über das logische Schließen I. Math. Z. 39, 176–210 (1935)
Howse, J., Stapleton, G., Taylor, J.: Spider diagrams. LMS J. Comput. Math. 8, 145–194 (2005)
Linker, S., Burton, J., Jamnik, M.: Tactical diagrammatic reasoning. In: UITP 2016. EPTCS, vol. 239, pp. 29–42. Open Publishing Association (2017)
Mineshima, K., Okada, M., Takemura, R.: Two types of diagrammatic inference systems: natural deduction style and resolution style. In: Goel, A.K., Jamnik, M., Narayanan, N.H. (eds.) Diagrams 2010. LNCS (LNAI), vol. 6170, pp. 99–114. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14600-8_12
Negri, S., von Plato, J., Ranta, A.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)
Shin, S.J.: The Logical Status of Diagrams. Cambridge University Press, Cambridge (1995)
Stapleton, G., Masthoff, J.: Incorporating negation into visual logics: a case study using Euler diagrams. In: VLC 2007, pp. 187–194. Knowledge Systems Institute (2007)
Urbas, M., Jamnik, M., Stapleton, G.: Speedith: a reasoner for spider diagrams. J. Log. Lang. Inform. 24(4), 487–540 (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Linker, S. (2018). Sequent Calculus for Euler Diagrams. In: Chapman, P., Stapleton, G., Moktefi, A., Perez-Kriz, S., Bellucci, F. (eds) Diagrammatic Representation and Inference. Diagrams 2018. Lecture Notes in Computer Science(), vol 10871. Springer, Cham. https://doi.org/10.1007/978-3-319-91376-6_37
Download citation
DOI: https://doi.org/10.1007/978-3-319-91376-6_37
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-91375-9
Online ISBN: 978-3-319-91376-6
eBook Packages: Computer ScienceComputer Science (R0)