A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
From MaRDI portal
Publication:2881098
DOI10.2168/LMCS-8(1:30)2012zbMath1238.68147arXiv1201.3601MaRDI QIDQ2881098
Publication date: 3 April 2012
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1201.3601
natural deductionformal mathematicsproof assistantsinteractive theorem provingtactics\texttt{HOL Light}\texttt{Mizar}\texttt{HOL}\texttt{miz3}declarative proof styleprocedural proof style
Related Items
Four decades of {\textsc{Mizar}}. Foreword ⋮ From informal to formal proofs in Euclidean geometry ⋮ Mizar: State-of-the-art and Beyond ⋮ CryptHOL: game-based proofs in higher-order logic ⋮ Formalizing Ordinal Partition Relations Using Isabelle/HOL ⋮ Formal analysis of optical systems ⋮ Declarative Proof Translation (Short Paper) ⋮ An introduction to mechanized reasoning ⋮ A formal semantics of nested atomic sections with thread escape ⋮ miz3 ⋮ Semantics of Mizar as an Isabelle object logic ⋮ A Vernacular for Coherent Logic ⋮ Formal Proofs for Nonlinear Optimization ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
