Two types of diagrammatic inference systems

Natural deduction style and resolution style

Koji Mineshima, Mitsuhiro Okada, Ryo Takemura

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

Since the 1990s, reasoning with Venn and Euler diagrams has been studied from mathematical and logical viewpoints. The standard approach to a formalization is a "region-based" approach, where a diagram is defined as a set of regions. An alternative is a "relation-based" approach, where a diagram is defined in terms of topological relations (inclusion and exclusion) between circles and points. We compare these two approaches from a proof-theoretical point of view. In general, diagrams correspond to formulas in symbolic logic, and diagram manipulations correspond to applications of inference rules in a certain logical system. From this perspective, we demonstrate the following correspondences. On the one hand, a diagram construed as a set of regions corresponds to a disjunctive normal form formula and the inference system based on such diagrams corresponds to a resolution calculus. On the other hand, a diagram construed as a set of topological relations corresponds to an implicational formula and the inference system based on such diagrams corresponds to a natural deduction system. Based on these correspondences, we discuss advantages and disadvantages of each framework.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages99-114
Number of pages16
Volume6170 LNAI
DOIs
Publication statusPublished - 2010
Event6th International Conference on the Theory and Application of Diagrams, Diagrams 2010 - Portland, OR, United States
Duration: 2010 Aug 92010 Aug 11

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6170 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other6th International Conference on the Theory and Application of Diagrams, Diagrams 2010
CountryUnited States
CityPortland, OR
Period10/8/910/8/11

Fingerprint

Natural Deduction
Diagram
Topological Relations
Correspondence
Style
Inference Rules
Formalization
Normal Form
Euler
Manipulation
Calculus
Circle
Reasoning
Inclusion
Logic

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Mineshima, K., Okada, M., & Takemura, R. (2010). Two types of diagrammatic inference systems: Natural deduction style and resolution style. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6170 LNAI, pp. 99-114). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6170 LNAI). https://doi.org/10.1007/978-3-642-14600-8_12

Two types of diagrammatic inference systems : Natural deduction style and resolution style. / Mineshima, Koji; Okada, Mitsuhiro; Takemura, Ryo.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6170 LNAI 2010. p. 99-114 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6170 LNAI).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Mineshima, K, Okada, M & Takemura, R 2010, Two types of diagrammatic inference systems: Natural deduction style and resolution style. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 6170 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6170 LNAI, pp. 99-114, 6th International Conference on the Theory and Application of Diagrams, Diagrams 2010, Portland, OR, United States, 10/8/9. https://doi.org/10.1007/978-3-642-14600-8_12
Mineshima K, Okada M, Takemura R. Two types of diagrammatic inference systems: Natural deduction style and resolution style. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6170 LNAI. 2010. p. 99-114. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-14600-8_12
Mineshima, Koji ; Okada, Mitsuhiro ; Takemura, Ryo. / Two types of diagrammatic inference systems : Natural deduction style and resolution style. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 6170 LNAI 2010. pp. 99-114 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{a04f8ddeca354b99ba20ae6c70a0dcff,
title = "Two types of diagrammatic inference systems: Natural deduction style and resolution style",
abstract = "Since the 1990s, reasoning with Venn and Euler diagrams has been studied from mathematical and logical viewpoints. The standard approach to a formalization is a {"}region-based{"} approach, where a diagram is defined as a set of regions. An alternative is a {"}relation-based{"} approach, where a diagram is defined in terms of topological relations (inclusion and exclusion) between circles and points. We compare these two approaches from a proof-theoretical point of view. In general, diagrams correspond to formulas in symbolic logic, and diagram manipulations correspond to applications of inference rules in a certain logical system. From this perspective, we demonstrate the following correspondences. On the one hand, a diagram construed as a set of regions corresponds to a disjunctive normal form formula and the inference system based on such diagrams corresponds to a resolution calculus. On the other hand, a diagram construed as a set of topological relations corresponds to an implicational formula and the inference system based on such diagrams corresponds to a natural deduction system. Based on these correspondences, we discuss advantages and disadvantages of each framework.",
author = "Koji Mineshima and Mitsuhiro Okada and Ryo Takemura",
year = "2010",
doi = "10.1007/978-3-642-14600-8_12",
language = "English",
isbn = "364214599X",
volume = "6170 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "99--114",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Two types of diagrammatic inference systems

T2 - Natural deduction style and resolution style

AU - Mineshima, Koji

AU - Okada, Mitsuhiro

AU - Takemura, Ryo

PY - 2010

Y1 - 2010

N2 - Since the 1990s, reasoning with Venn and Euler diagrams has been studied from mathematical and logical viewpoints. The standard approach to a formalization is a "region-based" approach, where a diagram is defined as a set of regions. An alternative is a "relation-based" approach, where a diagram is defined in terms of topological relations (inclusion and exclusion) between circles and points. We compare these two approaches from a proof-theoretical point of view. In general, diagrams correspond to formulas in symbolic logic, and diagram manipulations correspond to applications of inference rules in a certain logical system. From this perspective, we demonstrate the following correspondences. On the one hand, a diagram construed as a set of regions corresponds to a disjunctive normal form formula and the inference system based on such diagrams corresponds to a resolution calculus. On the other hand, a diagram construed as a set of topological relations corresponds to an implicational formula and the inference system based on such diagrams corresponds to a natural deduction system. Based on these correspondences, we discuss advantages and disadvantages of each framework.

AB - Since the 1990s, reasoning with Venn and Euler diagrams has been studied from mathematical and logical viewpoints. The standard approach to a formalization is a "region-based" approach, where a diagram is defined as a set of regions. An alternative is a "relation-based" approach, where a diagram is defined in terms of topological relations (inclusion and exclusion) between circles and points. We compare these two approaches from a proof-theoretical point of view. In general, diagrams correspond to formulas in symbolic logic, and diagram manipulations correspond to applications of inference rules in a certain logical system. From this perspective, we demonstrate the following correspondences. On the one hand, a diagram construed as a set of regions corresponds to a disjunctive normal form formula and the inference system based on such diagrams corresponds to a resolution calculus. On the other hand, a diagram construed as a set of topological relations corresponds to an implicational formula and the inference system based on such diagrams corresponds to a natural deduction system. Based on these correspondences, we discuss advantages and disadvantages of each framework.

UR - http://www.scopus.com/inward/record.url?scp=77955806284&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77955806284&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-14600-8_12

DO - 10.1007/978-3-642-14600-8_12

M3 - Conference contribution

SN - 364214599X

SN - 9783642145995

VL - 6170 LNAI

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 99

EP - 114

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -