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