Dr. Sven Linker, University of Brighton

Abstract:

In the verification of systems, most techniques concentrate on the mere existence of a proof, without much feedback for the users. However, a concrete proof is an important tool to convince humans that a theorem is indeed true. Hence it is beneficial, if a tool creates a proof for human inspection. Furthermore, it has been shown that in many instances, formal diagrammatic systems possess cognitive advantages compared to formal systems based on text.

In this talk, I will report on current work towards a notion of readability of diagrammatic proofs. To that end, I restrict myself to a rather simple language: formal Euler diagrams. We conducted an empirical study to examine the ability of humans to identify proof rule applications. Furthermore, we extended an existing diagrammatic theorem prover with means for proof search and for tactical reasoning inspired by the Isabelle framework. The implementation allows the user to examine the concrete proof.