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
- ALCOR
- ACL2
- Coq
- Isabelle
- LEO-II
- Proviola
- Title not available (Why is that?)
- Theorema
- ML
- TPS
- Title not available (Why is that?)
- Isabelle/HOL
- Vivid
- MizarMode
- Isabelle/Isar
- IsaPlanner
- CASL
- MPTP
- MPTP 0.2
- OTTER
- TADD
- VAMPIRE
- MAYA
- CoqEAL
- PVS
- MathWebSearch
- THF0
- gensim
- SPASS
- TPTP
- 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
- leanCoP
- SmallCheck
- TLAPS
- 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
