TY - GEN
T1 - Two types of diagrammatic inference systems
T2 - 6th International Conference on the Theory and Application of Diagrams, Diagrams 2010
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
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 99
EP - 114
BT - Diagrammatic Representation and Inference - 6th International Conference, Diagrams 2010, Proceedings
Y2 - 9 August 2010 through 11 August 2010
ER -