The readability of proofs in diagrammatic logic

Lead Research Organisation: University of Brighton
Department Name: Sch of Computing, Engineering & Maths

Abstract

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.

Planned Impact

The research outcomes will have significant benefits for a wide range of beneficiaries. Some of these benefits will be realised during the lifetime of the project or in the months after it ends, while some benefits will take several years to come to fruition. We anticipate that the project will benefit the following groups:

. Users of diagrammatic modelling systems in industry: examples include NOKIA, who have applied Euler-based logic developed by the Visual Modelling Group in privacy engineering. In the short-term, this group will benefit from increased awareness of and access to the potential role of reasoning (automated and interactive) within modelling processes such as ontology engineering. In the medium and long-term, this group will benefit from access to improved modelling processes through access to readable proofs, leading to better understanding
of aspects of the systems being modelled and to economic gains. Our work will enhance the communication of precise ideas within businesses, enabling non-mathematicians to
participate in reasoning activities via more accessible methods. Our research objectives will allow our industrial collaborators (such as NOKIA) to enrich society by providing software systems
with better designs.

. Developers and users of diagrammatic and/or heterogeneous reasoning: our collaborators at Stanford and Cambridge, the other developers and research teams who contribute to the Openbox and Speedith codebases, and the users of the software. This group will benefit from improved knowledge of integrating diagrammatic reasoning tools with Openbox. Our research objectives have the potential to attract more users and developers to the Openbox platform by offering a more diverse selection of components and, in the medium and long-term, enrich society by making courseware and source code of our tools available.

. Teachers and students of logic: those organisations and individuals who want to find accessible ways to teach the skills of reasoning in a logical system, and those students who may find diagrammatic or heterogeneous logic more accessible than the purely symbolic alternative. Our objectives will have an immediate benefit for this group by enabling the enhancement and extension of current methods of teaching analytical reasoning by improving the state-of-the-art of teaching tools based on diagrams. The research-based software tools we deliver will make analytical reasoning more accessible for those people with cognitive preferences for diagrammatic as opposed to symbolic reasoning. In the medium and long-term this has the potential to enrich society by making diagrammatic reasoning more accessible to wider groups of people, and provide the foundation for enhancing the digital economy by making it possible to improve
education in mathematical logic.

These impacts will be achieved by our commitment to make our results widely and freely available, and by publicising our work through public forums and user groups such as mailing lists relevant to Openbox and mathematical education.

Publications


10 25 50
Linker S (2017) Tactical Diagrammatic Reasoning in Electronic Proceedings in Theoretical Computer Science
 
Description We carried out the first empirical study that tries to establish which factors make diagrammatic proof rules easy or more difficult to understand. The findings of the study were that proof rules applied to less cluttered diagrams are easier to understand, relative to rules applied to more cluttered diagrams, and that we can categorise certain proof rules as "simple" or "complex". Unsurprisingly, the simple rules are easier to understand than the complex ones. In the next step, we are using these results to inform the development of a diagrammatic theorem prover. Our theorem prover uses "tactics", an approach which is often found in conventional theorem proving software but which has not been used in a diagrammatic context before. The tactics are designed to produce readable proofs, using the results of the study to do so.
Exploitation Route We are embedding the results of our study in diagrammatic theorem proving software which will run as a standalone application and also as a plugin for the heterogeneous (i.e. diagrammatic and symbolic logic) proof assistant Openproof.
Sectors Digital/Communication/Information Technologies (including Software),Education
URL http://readableproofs.org
 
Description Our findings were used to inform the development of software that allows tactical diagrammatic reasoning to be used in interactive educational material. This software is a plugin that makes our tactics available in Openbox, the software platform for teaching reasoning. It was developed by the project team during a visit to Dr Barker Plummer, whose research group at Stanford University produce Openbox. Work is ongoing to develop course material that uses Openbox and our plugin. We intend to present this course material as a tutorial at an appropriate Graduate School, such as the Indian Winter School on Diagrams (https://sites.google.com/site/winterschoolondiagrams2017/).
First Year Of Impact 2016
Sector Digital/Communication/Information Technologies (including Software),Education,Electronics
Impact Types Cultural,Societal
 
Description The Readability of Diagrammatic Proofs Project 
Organisation Stanford University
Country United States of America 
Sector Academic/University 
PI Contribution Myself and the RA on the project carried out the main body of work.
Collaborator Contribution Advice and guidance on concepts and theoretical direction. Software development. Co-authors on publications.
Impact Publications are still in preparation.
Start Year 2015
 
Description The Readability of Diagrammatic Proofs Project 
Organisation University of Cambridge
Department Computer Laboratory
Country United Kingdom of Great Britain & Northern Ireland (UK) 
Sector Academic/University 
PI Contribution Myself and the RA on the project carried out the main body of work.
Collaborator Contribution Advice and guidance on concepts and theoretical direction. Software development. Co-authors on publications.
Impact Publications are still in preparation.
Start Year 2015
 
Title Readith 
Description A diagrammatic theorem prover based on spider diagrams. Readith is based on Speedith, which was developed by Matej Urbas. We have extended the software to reflect our research findings on the readability of diagrammatic proofs, to make use of proof tactics and to generate proofs automatically. 
Type Of Technology Software 
Year Produced 2016 
Open Source License? Yes  
Impact We will adapt the OpenProof educational system for heterogeneous logic to allow the use of Readith when teaching logic. OpenProof has a worldwide user base, and this will enable us to reach those users, enhancing the educational environment of students and teachers. 
URL https://github.com/speedith/speedith
 
Description Indian Winter School on Diagrams 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact I am a co-organiser of the Indian Winter School on Diagrams which is a week long series of courses aimed at PhD students and Early Career Researchers on techniques and concepts used in diagrams research. At the latest Winter School I co-presented a course on the empirical evaluation of diagrams. The course used the study undertaken during this project as a running example and included a detailed exploration of the notion of the readability of diagrams and diagrammatic proofs.
Year(s) Of Engagement Activity 2015,2017
URL https://sites.google.com/site/winterschoolondiagrams2017/winter-school-program/empirically-evaluatin...