Metamath
From MaRDI portal
swMATH13309MaRDI QIDQ25224FDOQ25224
Author name not available (Why is that?)
Official website: http://us.metamath.org/
Cited In (51)
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- A formalization of Dedekind domains and class groups of global fields
- Towards a trustworthy semantics-based language framework via proof generation
- Metamath Zero: designing a theorem prover prover
- Computer proofs about finite and regular sets: The unifying concept of subvariance.
- A parametric, resource-bounded generalization of Löb's theorem, and a robust cooperation criterion for open-source game theory
- The language of formal mathematics Russell
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Improving stateful premise selection with transformers
- Generating custom set theories with non-set structured objects
- Conversion of HOL Light proofs into Metamath
- Pell's equation
- Semantic representation of general topology in the Wolfram language
- KANT/KASH
- MizarMode
- Isabelle/ZF
- AEtnaNova
- TRX
- cminor
- PhoX
- Referee
- Russell
- Smm
- Lean
- AUTO2
- miz3
- KJS
- IsarMathLib
- Algebraic Numbers
- Logic2CNF
- Verified Prover
- ProofPeer
- FOL_Harrison
- CoDe
- Jape
- SerAPI
- TreeRePair
- mathlib
- egg
- Zeta_3_Irrational
- Proof search algorithm in pure logical framework
- Pollack-inconsistency
- Goeland
- Gaussian_Integers
- Minkowskis_Theorem
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Semantics of Mizar as an Isabelle object logic
- Applicable mathematics in a minimal computational theory of sets
- Smm, the simplified metamath
- Hammering towards QED
This page was built for software: Metamath
