### 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 language | English |
---|---|

Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Pages | 99-114 |

Number of pages | 16 |

Volume | 6170 LNAI |

DOIs | |

Publication status | Published - 2010 |

Event | 6th International Conference on the Theory and Application of Diagrams, Diagrams 2010 - Portland, OR, United States Duration: 2010 Aug 9 → 2010 Aug 11 |

### Publication series

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

Volume | 6170 LNAI |

ISSN (Print) | 03029743 |

ISSN (Electronic) | 16113349 |

### Other

Other | 6th International Conference on the Theory and Application of Diagrams, Diagrams 2010 |
---|---|

Country | United States |

City | Portland, OR |

Period | 10/8/9 → 10/8/11 |

### Fingerprint

### ASJC Scopus subject areas

- Computer Science(all)
- Theoretical Computer Science

### Cite this

*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.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*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

}

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

AN - SCOPUS:77955806284

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 -