Interactive Proof Presentations with Cobra

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 audito...

Full description

Bibliographic Details
Main Authors: Martin Ring, Christoph Lüth
Format: Article
Language:English
Published: Open Publishing Association 2017-01-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1701.07127v1
id doaj-b74ef206a69344f5a6f6c365d03a3f2d
record_format Article
spelling doaj-b74ef206a69344f5a6f6c365d03a3f2d2020-11-24T22:32:40ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802017-01-01239Proc. UITP 2016435210.4204/EPTCS.239.4:4Interactive Proof Presentations with CobraMartin Ring0Christoph Lüth1 DFKI DFKI and Universität Bremen 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.http://arxiv.org/pdf/1701.07127v1
collection DOAJ
language English
format Article
sources DOAJ
author Martin Ring
Christoph Lüth
spellingShingle Martin Ring
Christoph Lüth
Interactive Proof Presentations with Cobra
Electronic Proceedings in Theoretical Computer Science
author_facet Martin Ring
Christoph Lüth
author_sort Martin Ring
title Interactive Proof Presentations with Cobra
title_short Interactive Proof Presentations with Cobra
title_full Interactive Proof Presentations with Cobra
title_fullStr Interactive Proof Presentations with Cobra
title_full_unstemmed Interactive Proof Presentations with Cobra
title_sort interactive proof presentations with cobra
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2017-01-01
description 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.
url http://arxiv.org/pdf/1701.07127v1
work_keys_str_mv AT martinring interactiveproofpresentationswithcobra
AT christophluth interactiveproofpresentationswithcobra
_version_ 1725732868796186624