Two types of diagrammatic inference systems: Natural deduction style and resolution style

Koji Mineshima, Mitsuhiro Okada, Ryo Takemura

研究成果: Conference contribution

10 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトルDiagrammatic Representation and Inference - 6th International Conference, Diagrams 2010, Proceedings
ページ99-114
ページ数16
DOI
出版ステータスPublished - 2010
イベント6th International Conference on the Theory and Application of Diagrams, Diagrams 2010 - Portland, OR, United States
継続期間: 2010 8 92010 8 11

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
6170 LNAI
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

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

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Two types of diagrammatic inference systems: Natural deduction style and resolution style」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル