A comparison of Mizar and Isar
From MaRDI portal
Publication:1868515
DOI10.1023/A:1021935419355zbMath1064.68083MaRDI QIDQ1868515
Publication date: 27 April 2003
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (17)
Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs ⋮ Four decades of {\textsc{Mizar}}. Foreword ⋮ Mizar: State-of-the-art and Beyond ⋮ A Brief Overview of Mizar ⋮ Supporting the formal verification of mathematical texts ⋮ Declarative representation of proof terms ⋮ A Declarative Language for the Coq Proof Assistant ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ The Isabelle Framework ⋮ Declarative Proof Translation (Short Paper) ⋮ A User Interface for a Mathematical System that Allows Ambiguous Formulae ⋮ Computer theorem proving in mathematics ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic ⋮ Semantics of Mizar as an Isabelle object logic ⋮ Logic-Free Reasoning in Isabelle/Isar ⋮ Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets
Uses Software
This page was built for publication: A comparison of Mizar and Isar
