miz3

MaRDI QIDQ30463swMATHFDO

Official website https://arxiv.org/pdf/1201.3601.pdf

Described by source

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

Cited in

(21)

• mizar-items
• MizarMode
• A formal semantics of nested atomic sections with thread escape
• CryptHOL: game-based proofs in higher-order logic
• Semantics of Mizar as an Isabelle object logic
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• From informal to formal proofs in Euclidean geometry
• CodeV
• Zemax
• LASCAD
• Four decades of \textsc{Mizar}. Foreword
• Mizar: state-of-the-art and beyond
• Zoo Probabilistic Systems
• Logic2CNF
• Formal analysis of optical systems
• Tarski geometry axioms
• Probabilistic_While
• MFMC_Countable
• Game_Based_Crypto
• A vernacular for coherent logic
• Declarative Proof Translation (Short Paper)

This page was built for software: miz3