swMATH4599MaRDI QIDQ16770FDOQ16770
Author name not available (Why is that?)
Official website: http://isabelle.in.tum.de/Isar/
Cited In (only showing first 100 items - show all)
- A graphical user interface for formal proofs in geometry
- Faster and more complete extended static checking for the Java modeling language
- A synthesis of the procedural and declarative styles of interactive theorem proving
- A Brief Overview of Mizar
- The Isabelle Framework
- Title not available (Why is that?)
- Isabelle
- Title not available (Why is that?)
- Theorema
- Rapide
- Prosper
- IMP++
- Title not available (Why is that?)
- Isabelle/HOL
- SecureUML
- MizarMode
- Isabelle/Isar
- IsaPlanner
- MAYA
- PVS
- MWB
- distcc
- Omnibus
- Mizar
- Cabri-geometry
- IsaWin
- Proof General
- Isabelle/ZF
- Netsoft
- TAS
- HOL
- TeXmacs
- HOL-OCL
- Matita
- AEtnaNova
- Saoithin
- Isabelle/jEdit
- PIDE
- CeTA
- HOL-Omega
- UTP2
- MML
- HOCL
- Sledgehammer
- ArgoCLP
- OMDoc
- Isabelle/PIDE
- LCF
- GF
- EAT
- jEdit
- ForTheL
- Proof General Kit
- CtCoq
- SmallCheck
- iJulienne
- SAD
- NaCl
- Pcoq
- PhoX
- PoplMark
- ProofWeb
- PRocH
- PROSPER
- SystemOnTPTP
- Poly/ML
- Nominal Isabelle
- Locales
- Referee
- Eisbach
- ConfiChair
- Metamath
- GF
- Hat
- CC-Pi
- seL4
- Xtext
- CoSMed
- miz3
- IsaFoL
- Lambda-Clam
- LOUI
- Plat-Omega
- XBarnacle
- LLFp
- Lifting
- ltl2dstar
- Multi
- Transfer
- SAD as a mathematical assistant -- how should we go from here to there?
- Nominal techniques in Isabelle/HOL
- The Matita interactive theorem prover
- Automatic proof and disproof in Isabelle/HOL
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Mizar: state-of-the-art and beyond
- Zeno: an automated prover for properties of recursive data structures
- AUTO2, a saturation-based heuristic prover for higher-order logic
- Metis
- Formalizing the Edmonds-Karp algorithm
- ProofScript: proof scripting for the masses
This page was built for software: Isar
