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
• 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
• Four decades of \textsc{Mizar}. Foreword
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Tarski geometry axioms
• Semantics of Mizar as an Isabelle object logic
• A vernacular for coherent logic
• Mizar: state-of-the-art and beyond

This page was built for software: miz3