A Framework for Interactive Proof

DOI10.1007/978-3-540-73086-6_15MaRDI QIDQ5428268zbMATH OpenOpenAlexFDO

Authors Christoph Lüth, Daniel Winterstein, D. Aspinall

Publication date 28 November 2007

Published in Towards Mechanized Mathematical Assistants (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73086-6_15

Mathematics Subject Classification ID

Recommendations

• scientific article; zbMATH DE number 1629953
• Interactive theorem proving from the perspective of Isabelle/Isar
• Isabelle/jEdit – A Prover IDE within the PIDE Framework
• The Isabelle Framework
• ProofViz: an interactive visual proof explorer

Cited in

(15)

• Interactive proofs for social graphs
• A logic of interactive proofs
• Automation for interactive proof: first prototype
• A graphical user interface for formal proofs in geometry
• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• scientific article; zbMATH DE number 1629956 (Why is no real title available?)
• Interactive Coding for Interactive Proofs
• A Review of Mathematical Knowledge Management
• An Interactive Driver for Goal-directed Proof Strategies
• Asynchronous proof processing with Isabelle/Scala and Isabelle/jEdit
• Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover's palette
• Isabelle as document-oriented proof assistant
• Interactive proofs in higher-order concurrent separation logic
• Combining Isabelle and QEPCAD-B in the Prover’s Palette
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors

Describes a project that uses

Uses Software

• IsaPlanner
• Mizar
• IsaWin
• Proof General
• Proof General Kit

This page was built for publication: A Framework for Interactive Proof

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