A Diagrammatic Inference System with Euler Circles

Koji Mineshima, Mitsuhiro Okada, Ryo Takemura

Research output: Contribution to journalArticle

17 Citations (Scopus)

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.

Original languageEnglish
Pages (from-to)365-391
Number of pages27
JournalJournal of Logic, Language and Information
Volume21
Issue number3
DOIs
Publication statusPublished - 2012 Jul

Fingerprint

Linguistics
Semantics
deduction
formalization
eighteenth century
semantics
linguistics
Leonhard Euler
Logic
Inference
Logicians
Diagrammatic Reasoning
Diagrams
Formalization
1990s
Natural Deduction
Unification
Completeness
Proof Theory

Keywords

  • Diagrammatic reasoning
  • Euler diagram
  • Proof-theory

ASJC Scopus subject areas

  • Linguistics and Language
  • Philosophy
  • Computer Science (miscellaneous)

Cite this

A Diagrammatic Inference System with Euler Circles. / Mineshima, Koji; Okada, Mitsuhiro; Takemura, Ryo.

In: Journal of Logic, Language and Information, Vol. 21, No. 3, 07.2012, p. 365-391.

Research output: Contribution to journalArticle

Mineshima, Koji ; Okada, Mitsuhiro ; Takemura, Ryo. / A Diagrammatic Inference System with Euler Circles. In: Journal of Logic, Language and Information. 2012 ; Vol. 21, No. 3. pp. 365-391.
@article{43579e0def1d45a6b5f21358a8fb7c7f,
title = "A Diagrammatic Inference System with Euler Circles",
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.",
keywords = "Diagrammatic reasoning, Euler diagram, Proof-theory",
author = "Koji Mineshima and Mitsuhiro Okada and Ryo Takemura",
year = "2012",
month = "7",
doi = "10.1007/s10849-012-9160-6",
language = "English",
volume = "21",
pages = "365--391",
journal = "Journal of Logic, Language and Information",
issn = "0925-8531",
publisher = "Springer Netherlands",
number = "3",

}

TY - JOUR

T1 - A Diagrammatic Inference System with Euler Circles

AU - Mineshima, Koji

AU - Okada, Mitsuhiro

AU - Takemura, Ryo

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

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 -