Proviola: a tool for proof re-animation

DOI10.1007/978-3-642-14128-7_37MaRDI QIDQ3582730zbMATH OpenOpenAlexFDO

Authors Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk

Publication date 24 August 2010

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1005.2672

Mathematics Subject Classification ID

Abstract: To improve on existing models of interaction with a proof assistant (PA), in particular for storage and replay of proofs, we in- troduce three related concepts, those of: a proof movie, consisting of frames which record both user input and the corresponding PA response; a camera, which films a user's interactive session with a PA as a movie; and a proviola, which replays a movie frame-by-frame to a third party. In this paper we describe the movie data structure and we discuss a proto- type implementation of the camera and proviola based on the ProofWeb system. ProofWeb uncouples the interaction with a PA via a web- interface (the client) from the actual PA that resides on the server. Our camera films a movie by "listening" to the ProofWeb communication. The first reason for developing movies is to uncouple the reviewing of a formal proof from the PA used to develop it: the movie concept enables users to discuss small code fragments without the need to install the PA or to load a whole library into it. Other advantages include the possibility to develop a separate com- mentary track to discuss or explain the PA interaction. We assert that a combined camera+proviola provides a generic layer between a client (user) and a server (PA). Finally we claim that movies are the right type of data to be stored in an encyclopedia of formalized mathematics, based on our experience in filming the Coq standard library.

Recommendations

• ProofViz: an interactive visual proof explorer
• Towards the animation of proofs -- testing proofs by examples
• scientific article; zbMATH DE number 1629953
• scientific article; zbMATH DE number 2090059
• Web interfaces for proof assistants

Cited in

(8)

• ProofViz: an interactive visual proof explorer
• Towards Knowledge Management for HOL Light
• Proviola
• Web interfaces for proof assistants
• Large formal wikis: issues and solutions
• Isabelle as document-oriented proof assistant
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
• Towards the animation of proofs -- testing proofs by examples

Describes a project that uses

Uses Software

• ProofWeb
• Matita
• Isabelle/Isar
• Coq

This page was built for publication: Proviola: a tool for proof re-animation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3582730)