Submitted: September 2014
Abstract
In order to help beginner students in computer science with taking their first steps into the realm of formal mathematical proofs, the interactive graphical proof assistant edupa has been developed. It displays basic mathematical proofs in a special form of directed graphs. The goal of this thesis is to show how these “proof graphs” can be drawn automatically, in order to achieve decent layouts without distracting the user from the actual task of constructing the proof.
We give an overview of edupa’s functionality as well as a formal definition of the concept of proof graphs as a means of representing mathematical proofs. We state requirements a layouting algorithm for proof graphs should fulfill and evaluate existing general approaches to graph layouting with regard to their ability of meeting these requirements.
To compensate the shortcomings of existing approaches for our specific problem, we propose a force-directed graph drawing algorithm that aims at making use of the characteristic features of proof graphs. Our goal is not only to provide aesthetically pleasing results, but also to account for the interactivity of the edupa concept, by keeping the layout reasonably stable throughout the sequence of user modifications.