Interactive Proof Presentations with Cobra
Logic in Computer Science
2017-01-26 v1
Abstract
We present Cobra, a modern 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 for live changes both by the presenter and the audience.
Keywords
Cite
@article{arxiv.1701.07127,
title = {Interactive Proof Presentations with Cobra},
author = {Martin Ring and Christoph Lüth},
journal= {arXiv preprint arXiv:1701.07127},
year = {2017}
}
Comments
In Proceedings UITP 2016, arXiv:1701.06745