A Drag-and-Drop Proof Tactic
summary
A browser-playable prototype called Actima prototype implements drag-and-drop proof steps backed by deep inference and subformula linking, claiming deterministic rewrite behaviors for any two subpropositions when they unify. It supports backward and forward moves, quantifier instantiation or under-quantifier modification, equality rewriting with multi-occurrence selection, and conditional rewrites that emit side conditions. The prototype exists and works for small examples; integration with Isabelle/Coq and robust proof replay remain future work.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:15Deep Inference
- 2:57Quantifiers
- 3:39Existential Quantifiers
- 7:20Conditional Rewriting
- 7:44Conclusions To Finish
- 8:29Directions of Future Work
related talks
26mIntegrating graphical proofs in Coq
24mActema: Integrating Graphical Proofs into ITPs via Plugin-Driven Gestural Interaction
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
21mLive Verification in an Interactive Proof Assistant
01h 10mMedium-scale automation for proof assistants
24mA Counterexample-Guided Debugger for Non-Recursive Datalog
16mIncremental Proof Development in Dafny with Module-Based Induction
22mA diagram editor to mechanize categorical proofs