Interactive Proof Presentations with Cobra

Martin Ring; Christoph Lüth

In: Serge Autexier; Pedro Queresma (Hrsg.). Workshop on User Interfaces for Theorem Provers (UITP2016). User Interfaces for Theorem Provers (UITP-2016), located at International Joint Conference on Automated Reasoning IJCAR 2016, July 2, Coimbra, Portugal, Pages 43-52, Electronic Proceedings in Theoretical Computer Science (EPTCS), Vol. 239, Open Publishing Association, 1/2017.


We present Cobra, a modern code and proof presentation framework, leveraging cutting-edge presentation technology together with a state of the art interactive theorem prover to present formalized mathematics as active documents. Cobra provides both an easy way to present proofs and a novel approach to auditorium interaction. The presentation is checked live by the theorem prover, and moreover allows live changes both by the presenter as well as the audience.


main.pdf (pdf, 237 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence