Metamath Zero: designing a theorem prover prover

DOI10.1007/978-3-030-53518-6_5zbMath1455.68243arXiv1910.10703OpenAlexW3042577812MaRDI QIDQ2219381

Yanyan Li

Publication date: 20 January 2021

Full work available at URL: https://arxiv.org/abs/1910.10703

zbMATH Keywords

verificationmetamathematicsformalization of mathematicsformal proofMetamath Zero

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (3)

Isabelle's metalogic: formalization and proof checker ⋮ Metamath Zero ⋮ A formalization and proof checker for Isabelle's metalogic

Uses Software

• Coq
• Isabelle/HOL
• HOL Light
• CakeML
• Metamath
• VST-Floyd
• Rust

This page was built for publication: Metamath Zero: designing a theorem prover prover