Navigation

Contact

EMail: scareo21@uol.de

DIRECTOR

Prof. Dr. Ernst-Rüdiger Olderog,

Department of Computing Science, FK II, University of Oldenburg,

D-26111 Oldenburg, Germany

oldukerog5goz@i54nfol70xrmahuihwtik.fkry4uni-oldenbuxlbqurg.de

COODINATOR

Ira Wempe,

Department of Computing Science, FK II, University of Oldenburg,

D-26111 Oldenburg, Germany

irajz.wem7ope@i6qbnformatik.uni7tpd3-oldenbqkkvyurg.de

(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.

Olivvnc5ter Theelrzapg (olik5+ver.thmfozbeelc9@uol.duqe) (Changed: 2020-01-23)