The readability of proofs in diagrammatic logic

图解逻辑证明的可读性

• 批准号: EP/M011763/1
• 负责人: Jim Burton
• 金额: $ 12.54万
• 依托单位: University of Brighton
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2015
• 资助国家: 英国
• 起止时间: 2015 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FM011763%2F1
• 关键词: readability; proofs; diagrammatic; logic

The fact that diagrams can be an expressive and accessible way to communicate is widely recognised and valued, but what makes one diagram more effective than another is seldom measured. Formal diagrams attempt to combine the effectiveness of graphics with mathematical logic, and have the potential to bring the benefits of this expressiveness and accessibility to the field of logical reasoning. Diagrammatic reasoning (or visual logic) consists of using diagrams to represent logical theorems and to create diagrammatic proofs or counter-arguments for those theorems. In this project we will analyse and measure, for the first time, the factors that affect comprehension in diagrammatic reasoning. Our research question is as follows: is it possible to develop a systematic understanding of readability in diagrammatic proofs? (We use the term "readable" to mean easy to understand and use.) To be effective, such understanding would yield strategies to be used to automatically construct readable proofs. Furthermore, these strategies should be general enough to be applied to any visual logic and possess predictive qualities that can inform the design of future visual logics.Euler diagrams are a simple visual logic which is used to represent data in a great many contexts. As well as being used informally or semi-formally in fields such as education, Euler diagrams have been used as a formal logic since the 1990s. The widespread use of Euler diagrams (for instance, in teaching set theory to school children) testifies to the fact that they are generally considered easy to understand. Logicians, philosophers and cognitive scientists have attempted to describe the origins of this ease of understanding, but have not done so in the specific context of the use of Euler diagrams in proofs, or in a way that yields general strategies for creating Euler diagram proofs which are easily understood.The aims of this project are to provide a detailed, formal understanding of readability in diagrammatic proofs and to provide ways of automatically generating readable diagrammatic proofs. We will achieve the second of these aims by adapting an existing automated Euler diagram theorem prover. The aims allow us to address what we believe to be two of the most challenging issues for the diagrams community today: the need to explore when diagrammatic reasoning is understandable by people, and the need to produce effective software tools that make the benefits of diagrams available to a wide range of people. The project addresses the need to categorise and to empirically measure the features that make diagrammatic proofs more, or less, easy to understand. Identifying these features and the ways in which they interact will help us to make better use of existing notations and design more effective logics in the future.

事实上，图表是一种表达能力强、易于理解的交流方式，这一点得到了广泛的认可和重视，但是，是什么让一个图表比另一个图表更有效，却很少被衡量出来。形式图试图将图形的有效性与数学逻辑结合起来，并有可能将这种表达性和可访问性的好处带到逻辑推理领域。图解推理（或视觉逻辑）包括使用图表来表示逻辑定理，并为这些定理创建图解证明或反论证。在这个项目中，我们将首次分析和测量影响图解推理理解的因素。我们的研究问题如下：是否有可能对图解证明的可读性有一个系统的理解？（我们使用“可读”一词是指易于理解和使用。）为了有效，这种理解将产生用于自动构建可读证明的策略。此外，这些策略应该足够通用，可以应用于任何视觉逻辑，并具有预测特性，可以为未来视觉逻辑的设计提供信息。欧拉图是一种简单的可视化逻辑，用于在许多情况下表示数据。除了在教育等领域非正式或半正式地使用外，欧拉图自20世纪90年代以来一直被用作正式逻辑。欧拉图的广泛使用（例如，在向学生教授集合论时）证明了这样一个事实，即欧拉图通常被认为是容易理解的。逻辑学家、哲学家和认知科学家试图描述这种易于理解的起源，但没有在证明中使用欧拉图的具体背景下这样做，或者以一种产生易于理解的欧拉图证明的一般策略的方式这样做。这个项目的目的是提供对图解证明可读性的详细、正式的理解，并提供自动生成可读图解证明的方法。我们将通过采用现有的自动欧拉图定理证明器来实现第二个目标。这些目标使我们能够解决我们认为是当今图表社区最具挑战性的两个问题：需要探索图表推理何时可以被人们理解，以及需要生产有效的软件工具，使图表的好处能够为更广泛的人所利用。该项目解决了对使图解证明更容易理解或更不容易理解的特征进行分类和经验度量的需要。识别这些特征及其交互方式将帮助我们更好地利用现有的符号，并在将来设计更有效的逻辑。

项目成果

Generating readable diagrammatic proofs

生成可读的图解证明

• DOI: 10.1109/vlhcc.2015.7357240
• 发表时间: 2015
• 作者: Burton J

Presence and Absence of Individuals in Diagrammatic Logics: An Empirical Comparison

图解逻辑中个体的存在和不存在：实证比较

• DOI: 10.1007/s11225-017-9711-6
• 发表时间: 2017
• 期刊: Studia Logica
• 影响因子: 0.7
• 作者: Stapleton G

Tactical Diagrammatic Reasoning

战术图解推理

• DOI: 10.4204/eptcs.239.3
• 发表时间: 2017
• 期刊: Electronic Proceedings in Theoretical Computer Science
• 作者: Linker S