A Framework for Interactive Proof

DOI10.1007/978-3-540-73086-6_15zbMath1202.68371OpenAlexW2166604183MaRDI QIDQ5428268

Daniel Winterstein, Christoph Lüth, David 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

Related Items

A graphical user interface for formal proofs in geometry ⋮ 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 ⋮ A Review of Mathematical Knowledge Management ⋮ Combining Isabelle and QEPCAD-B in the Prover’s Palette

Uses Software

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