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.
- The language of formal mathematics Russell
- A parametric, resource-bounded generalization of Löb's theorem, and a robust cooperation criterion for open-source game theory
- 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
- Semantic representation of general topology in the Wolfram language
- Pell's equation
- 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
- 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
- Gaussian_Integers
- Minkowskis_Theorem
- Hammering towards QED
This page was built for software: Metamath
