Abstract
Proof-theory has traditionally been developed based on linguistic (symbolic) representations of logical proofs. Recently, however, logical reasoning based on diagrammatic or graphical representations has been investigated by logicians. Euler diagrams were introduced in the eighteenth century. But it is quite recent (more precisely, in the 1990s) that logicians started to study them from a formal logical viewpoint. We propose a novel approach to the formalization of Euler diagrammatic reasoning, in which diagrams are defined not in terms of regions as in the standard approach, but in terms of topological relations between diagrammatic objects. We formalize the unification rule, which plays a central role in Euler diagrammatic reasoning, in a style of natural deduction. We prove the soundness and completeness theorems with respect to a formal set-theoretical semantics. We also investigate structure of diagrammatic proofs and prove a normal form theorem.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Blackett D. W. (1983) Elementary topology. Academic Press, London
Euler, L. (1768). Lettres à une Princesse d’Allemagne sur Divers Sujets de Physique et de Philosophie, Saint-Pétersbourg: De l’Académie des Sciences. (H. Hunter, Letters of Euler to a German Princess on Different Subjects in Physics and Philosophy, Thoemmes Press, 1997, English trans.).
Gentzen, G. (1934). Untersuchungen über das logische Schließen, Mathematische Zeitschrift, 39, 176–210, 405–431. (Investigations into logical deduction. In M. E. Szabo (ed.), The collected Papers of Gerhard Gentzen, 1969, English trans.).
Hammer E. (1995) Logic and visual information. CSLI Publications, Stanford, CA
Hammer E., Danner N. (1996) Towards a model theory of diagrams. Journal of Philosophical Logic 25(5): 463–482
Hammer E., Shin S.-J. (1998) Euler’s visual logic. History and Philosophy of Logic 19: 1–29
Howse, J., Molina, F., & Taylor, J. (2000). SD2: A sound and complete diagrammatic reasoning system. In 2000 IEEE international symposium on visual languages, (pp. 127–134).
Howse J., Stapleton G., Taylor J. (2005) Spider diagrams. LMS Journal of Computation and Mathematics 8: 145–194
Mineshima, K., Okada, M., & Takemura, R. (2009). Conservativity for a hierarchy of Euler and Venn reasoning systems. In Proceedings of visual languages and logic 2009, CEUR series (Vol. 510, pp. 37–61).
Mineshima, K., Okada, M., & Takemura, R. (2010). Two types of diagrammatic inference systems: Natural deduction style and resolution style. In Diagrammatic representation and inference: 6th international conference, Diagrams 2010, lecture notes in artificial intelligence, Springer (pp. 99–114).
Molina, F. (2001). Reasoning with extended Venn–Peirce diagrammatic systems. Ph.D. thesis, University of Brighton.
Okada M. (1999) Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic. Theoretical Computer Science 227(1–2): 333–396
Peirce, C. S. (1933). In C. Hartshorne, & P. Weiss (Eds.), Collected papers of Charles Sanders Peirce (Vol. 4). Cambridge, MA: Harvard University Press.
Sato, Y., Mineshima, K., & Takemura, R. (2010). The efficacy of Euler and Venn diagrams in deductive reasoning: Empirical findings. In Diagrammatic representation and inference: 6th international conference, Diagrams 2010, lecture notes in artificial intelligence, Springer (pp. 6–22).
Shin S.-J. (1994) The logical status of diagrams. Cambridge University Press, Cambridge, MA
Stapleton, G. (2005). A survey of reasoning systems based on Euler diagrams. In Proceedings of the first international workshop on Euler diagrams (Euler 2004), electronic notes in theoretical computer science (Vol. 134, pp. 127–151).
Stapleton, G., Howse, J., Rodgers, P., & Zhang, L. (2008). Generating Euler diagrams from existing layouts. In Layout of (software) engineering diagrams 2008, electronic communications of the EASST, (Vol. 13, pp. 16–31).
Stapleton G., Rodgers P., Howse J., Zhang L. (2011) Inductively generating Euler diagrams. IEEE Transactions on Visualization and Computer Graphics 17(1): 88–100
Swoboda N., Allwein G. (2004) Using DAG transformations to verify Euler/Venn homogeneous and Euler/Venn FOL heterogeneous rules of inference. Journal on Software and System Modeling 3(2): 136–149
Venn J. (1881) Symbolic logic. Macmillan, London
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Mineshima, K., Okada, M. & Takemura, R. A Diagrammatic Inference System with Euler Circles. J of Log Lang and Inf 21, 365–391 (2012). https://doi.org/10.1007/s10849-012-9160-6
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10849-012-9160-6