ProofViz: an interactive visual proof explorer

DOI10.1007/978-3-030-83978-9_6MaRDI QIDQ832103zbMATH OpenOpenAlexFDO

Authors N. E. Zubov

Publication date 25 March 2022

Full work available at URL https://doi.org/10.1007/978-3-030-83978-9_6

zbMATH Keywords

proof assistantsGUI toolsIDEs

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Panoptes: an exploration tool for formal proofs
• Visual theorem proving with the Incredible Proof Machine
• The RISC ProofNavigator: a proving assistant for program verification in the classroom
• scientific article; zbMATH DE number 1629953
• Proviola: a tool for proof re-animation

Cites work

• scientific article; zbMATH DE number 2086496 (Why is no real title available?)
• Functionality in Combinatory Logic
• HACL*
• Inductive families
• Traf: a graphical proof tree viewer cooperating with Coq through Proof General
• Type systems as macros

Cited in

(18)

• An interactive derivation viewer
• Traf: a graphical proof tree viewer cooperating with Coq through Proof General
• A graphical language for proof strategies
• \textsf{Globular}: an online proof assistant for higher-dimensional rewriting
• scientific article; zbMATH DE number 2090059 (Why is no real title available?)
• The RISC ProofNavigator: a proving assistant for program verification in the classroom
• Click'n prove: interactive proofs within set theory
• Visual theorem proving with the Incredible Proof Machine
• scientific article; zbMATH DE number 1765686 (Why is no real title available?)
• ProofViz
• A Framework for Interactive Proof
• MikiBeta : A General GUI Library for Visualizing Proof Trees
• Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
• Proviola: a tool for proof re-animation
• Tool support for proof engineering
• Panoptes: an exploration tool for formal proofs
• VizAR: visualization of automated reasoning proofs (system description)
• Towards the animation of proofs -- testing proofs by examples

Describes a project that uses

Uses Software

• HACL*
• LOUI
• PVS

This page was built for publication: ProofViz: an interactive visual proof explorer

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