A drag-and-drop proof tactic
Pablo Donato (LIX, PARTOUT), Pierre-Yves Strub (LIX), Benjamin Werner, (LIX, PARTOUT)

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
