Actema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction
summary
Actema is a prototype GUI that integrates with Rocq via a client-server plugin and exposes a web frontend (JS) and OCaml backend to build proofs by click and drag-and-drop gestures. The demo constructs and replays a proof of insertion preserving list sortedness, records gesture sequences into files, compiles them into tactics and produces a valid proof term; some UI and replay bugs remain. The authors claim gestural actions are a sound-and-complete proof system and support recorded actions replayed into Rocq tactics.
AI-written summary · about
chapters (10)
- 0:00Actima introduction
- 1:04Plugin setup in Rocq
- 3:40Proof with Actima
- 5:06Base case solving
- 7:13Case analysis
- 9:06Proof actions replay
- 10:10Lemma drag-and-drop
- 13:01Actima interaction
- 14:30Architecture of Actima and Rocq integration
- 18:08Conclusion
related talks
26mIntegrating graphical proofs in Coq
13mA Drag-and-Drop Proof Tactic
01h 10mMedium-scale automation for proof assistants
21mLive Verification in an Interactive Proof Assistant
22mA diagram editor to mechanize categorical proofs
19mQED in Context: An Observation Study of Proof Assistant Users
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
42mTaqueria: A new way to build on Tezos