IMPROOF

We aim to find universal mechanisms for interactive proof development that are based on Direct Manipulation. The goal is to employ rich user input devices such as mice, (multi-) touch screens, 3D graphical displays, virtual reality harnesses, etc. and to exploit the rich variety of interactive actions they enable to make interactive theorem proving easier for novices and powerful for experts. The project focuses both on the foundational aspects of interactive theorem proving by direct manipulation, enlarging its applicability to general deductive systems, and also on practical backend-agnostic prototypes that can support rich user interactions independent of textual interfaces.