Contact

Director

Prof. Dr. Ernst-Rüdiger Olderog

Department of Computing Science
FK II
University of Oldenburg
D-26111 Oldenburg, Germany

Coordinator

Ira Wempe

Department of Computing Science
FK II
University of Oldenburg
D-26111 Oldenburg, Germany

Dr. Sven Linker

(Semi-)Automation of Diagrammatic Theorem-proving with Consideration of Readability

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.

(Changed: 20 Jun 2024)  | 
Zum Seitananfang scrollen Scroll to the top of the page