Mizar
From MaRDI portal
swMATH4704MaRDI QIDQ16873FDOQ16873
Author name not available (Why is that?)
Official website: http://mizar.org/system/
Cited In (only showing first 100 items - show all)
- MMTTeX: connecting content and narration-oriented document formats
- A synthesis of the procedural and declarative styles of interactive theorem proving
- System for Automated Deduction (SAD): A Tool for Proof Verification
- Mining the Archive of Formal Proofs
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- GABLE
- Clados
- Locales
- Referee
- Jitawa
- Easychair
- MathHub.info
- Metamath
- GF
- WolframAlpha
- E-MaLeS
- Lean
- SigmaKEE
- seL4
- URSA
- SInE
- BliStr
- AUTO2
- HOL Zero
- OMEGA
- AGORA
- BliStrTune
- miz3
- Lambda-Clam
- LATIN
- Plat-Omega
- SNARK
- Idris
- NetSketch
- theoremprover-museum
- XBarnacle
- MSC
- Markdown
- Lifting
- Mathfind
- FEMaLeCoP
- Delphin
- KOMET
- MathLang
- Medmaker
- scunac
- OTT2MIZ
- webLurch
- SEPIA
- VMEXT
- Transfer
- SRASS
- ProofTool
- IsarMathLib
- Jordan
- vis.js
- kepler98
- MMode
- GitLab
- SWT
- Aligator.jl
- MathTools
- RISCAL
- FINANCE5
- OpenNMT
- DeepMath
- FraCaS
- sTeX
- AVL trees
- Cayley-Hamilton
- Archive Formal Proofs
- Berlekamp Zassenhaus
- Naproche
- ATPboost
- AVATAR
- Echelon Form
- Graph Theory
- ENIGMA
- Jordan Normal Forms
- Fuzz
- Liouville numbers
- EPGY
- Logic2CNF
- NASA PVS
- QR Decomposition
- Proofwatch
- Tame Graphs
- TacticToe
- Twee
- Treaps
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck}
- SAD as a mathematical assistant -- how should we go from here to there?
- Hammer for Coq: automation for dependent type theory
- The Lean theorem prover (system description)
- AUTO2, a saturation-based heuristic prover for higher-order logic
- ProofWatch: watchlist guidance for large theories in E
- ATPboost: learning premise selection in binary setting with ATP feedback
- Introduction to stopping time in stochastic finance theory. II
This page was built for software: Mizar
