A drag-and-drop proof tactic

TL;DR

This paper introduces a drag-and-drop proof tactic that leverages gestural user interface actions for intuitive and rapid formal proof construction, based on deep inference and previous pointing-based methods.

Contribution

It presents a novel proof construction approach using drag-and-drop gestures, integrating deep inference techniques and previous pointing ideas.

Findings

Proof steps can be associated with drag-and-drop actions.

The approach offers a quick and intuitive proof-building process.

It combines deep inference with gestural interface design.

Abstract

We explore the features of a user interface where formal proofs can be built through gestural actions. In particular, we show how proof construction steps can be associated to drag-and-drop actions. We argue that this can provide quick and intuitive proof construction steps. This work builds on theoretical tools coming from deep inference. It also resumes and integrates some ideas of the former proof-by-pointing project.