A Diagrammatic Reasoning System with Euler Circles
Koji Mineshima, Mitsuhiro Okada, Ryo Takemura · 2009
This paper is concerned with Euler diagrammatic reasoning. 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 many logicians. Euler diagrams were introduced in the 18th century by Leonhard Euler [1768]. But it is quite recent (more precisely, in the 1990s) that logicians started to study them from a formal logical viewpoint, and there are only few proof-theoretical investigations. Accordingly, in order to ll this gap, we formalize an Euler diagrammatic inference system and prove the soundness and completeness theorems with respect to a formal set-theoretical semantics. We further consider, from a proof-theoretical viewpoint, the structure of diagrammatic proofs and manners of their construction.