Diagrammatic Reasoning System with Euler Circles: Theory and Experiment Design

This paper is concerned with Euler diagrammatic reasoning. Proof-theory has tradi-tionally 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 the-orems 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. Contents