UITP 2016

We are really pleased to have a paper on our work on diagrammatic tactics accepted at UITP 2016, which is an IJCAR workshop. Sven will be giving a talk and demo at the workshop. The paper is called Tactical Diagrammatic Reasoning, and here’s the abstract:

Although automated reasoning with diagrams has been possible for some years, tools for diagrammatic reasoning are generally much less sophisticated than their sentential cousins. The tasks of exploring levels of automation and abstraction in the construction of proofs and of providing explanations of solutions expressed in the proofs remain to be addressed. In this paper we take an interactive proof assistant for Euler diagrams, Speedith, and add tactics to its
reasoning engine, providing a level of automation in the construction of proofs. By adding tactics to Speedith’s repertoire of inferences, we ease the interaction between the user and the system and capture a higher level explanation of the essence of the proof. We analysed the design options for tactics by using metrics which relate to human readability, such as the number of inferences and the amount of clutter present in diagrams. Thus, in contrast to the normal case with sentential tactics, our tactics are designed to not only prove the theorem, but also to support explanation.

Speedith

You will find a zip file containing the 2016 version of Speedith at the following link:

speedith-2016

Extract the archive. This will create the Speedith executable, speedith.jar and a folder with examples.

 

Please follow these instructions:

To use Speedith with Euler diagrams, please open the Preferences
(File->Preferences) on the first Startup.

  1. Tab Diagram Type: Choose Euler Diagrams
  2. Tab Tactics: Check Show low level-tactics if you want to see/apply all
    possible tactics provided by Speedith. Otherwise, only the high-level
    tactics (Venn (Depth), Venn (Breadth) and Copy Shading and Contours) will
    be available.
  3. Tab Auto Prover: Check that the automatic proof search in the background
    is switched of. The implementation of the automatic prover is only a prototype and tends to use up all memory that is available.

 

Examples of both proofs and proof goals are contained in the examples folder. The subfolder paper contains all proofs and proof goals mentioned in the submission to UITP 2016.

 

Requirements: Java 7

(Speedith has not been tested with Java 8. It might work or it might not.)

 

This version of Speedith has been compiled and tested on Ubuntu 16.04 (LTS). It should work on MacOS and Windows as long as a Java Runtime Environment is present, but we cannot give any guarantees.

Introduction

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.