miz3

swMATH18631MaRDI QIDQ30463FDOQ30463

Author name not available (Why is that?)

Described by source

• A synthesis of the procedural and declarative styles of interactive theorem proving

Cited In (11)

• A formal semantics of nested atomic sections with thread escape
• Mizar: State-of-the-art and Beyond
• Four decades of {\textsc{Mizar}}. Foreword
• From informal to formal proofs in Euclidean geometry
• Declarative Proof Translation (Short Paper)
• CryptHOL: game-based proofs in higher-order logic
• Formal analysis of optical systems
• A Vernacular for Coherent Logic
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Tarski geometry axioms
• Semantics of Mizar as an Isabelle object logic

This page was built for software: miz3