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.
翻译:我们探索了用户界面的特征, 正式的证明可以通过动态动作建立。 特别是, 我们展示了证据构建步骤如何可以与拖放行动联系起来。 我们争论说, 这可以提供快速和直觉的证明构建步骤。 这项工作建立在来自深层推理的理论工具之上。 它还恢复并整合了前校对项目的一些想法 。