English

A drag-and-drop proof tactic

Human-Computer Interaction 2022-11-08 v2 Logic in Computer Science

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.

Keywords

Cite

@article{arxiv.2210.11820,
  title  = {A drag-and-drop proof tactic},
  author = {Pablo Donato and Pierre-Yves Strub and Benjamin Werner},
  journal= {arXiv preprint arXiv:2210.11820},
  year   = {2022}
}
R2 v1 2026-06-28T04:09:44.864Z