TY - JOUR
T1 - A Diagrammatic Inference System with Euler Circles
AU - Mineshima, Koji
AU - Okada, Mitsuhiro
AU - Takemura, Ryo
N1 - Copyright:
Copyright 2012 Elsevier B.V., All rights reserved.
PY - 2012/7
Y1 - 2012/7
N2 - 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.
AB - 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.
KW - Diagrammatic reasoning
KW - Euler diagram
KW - Proof-theory
UR - http://www.scopus.com/inward/record.url?scp=84862174730&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84862174730&partnerID=8YFLogxK
U2 - 10.1007/s10849-012-9160-6
DO - 10.1007/s10849-012-9160-6
M3 - Article
AN - SCOPUS:84862174730
VL - 21
SP - 365
EP - 391
JO - Journal of Logic, Language and Information
JF - Journal of Logic, Language and Information
SN - 0925-8531
IS - 3
ER -