swMATH4704MaRDI QIDQ16873FDOQ16873
Author name not available (Why is that?)
Official website: http://mizar.org/system/
Cited In (only showing first 100 items - show all)
- User interaction with the Matita proof assistant
- Collaborative Interactive Theorem Proving with Clide
- The Isabelle Framework
- LEO-II
- Title not available (Why is that?)
- Theorema
- ML
- TPS
- Title not available (Why is that?)
- Vivid
- MizarMode
- CASL
- MPTP 0.2
- MAYA
- SPASS
- Isar
- MoMM
- LPL software
- IsaWin
- Proof General
- Isabelle/ZF
- Prover9
- TAS
- HOL
- ASCIIMathML
- Kaprekar Series Generator
- TeXmacs
- Matita
- ETPS
- AEtnaNova
- ActiveMath
- ProofPower
- Isabelle/jEdit
- PIDE
- HOL Light
- HOL-Omega
- C-CoRN
- Nuprl
- Satallax
- Mace4
- MML
- Hets
- Zenon
- Automath
- Sledgehammer
- Clide
- MMT
- ML4PG
- Twelf
- OMDoc
- Isabelle/PIDE
- QMT
- MaLeCoP
- TNTBase
- MathJax
- Polar
- STEXIDE
- MaSh
- LCF
- ALF
- GF
- EAT
- IMPS
- NZMATH
- Coq/SSReflect
- Agda
- gaia
- CalcCheck
- Tipi
- EgoMath
- Mella
- ForTheL
- leanCoP
- MD-jeep
- CtCoq
- SmallCheck
- SAD
- TLAPS
- PhoX
- E Theorem Prover
- Flyspeck
- ProofWeb
- PRocH
- MaLARea
- Analytica
- Monotonox
- Tsukuba
- SystemOnTPTP
- Poly/ML
- Coquelicot
- HOLyHammer
- FoCaLiZe
- MPTP-motivation, implementation, first experiments
- MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
- MPTP 0.2: Design, implementation, and initial experiments
- The Matita interactive theorem prover
- Automatic proof and disproof in Isabelle/HOL
- Tools for MML environment analysis
- Metis
- Coquelicot: a user-friendly library of real analysis for Coq
This page was built for software: Mizar
