swMATH6580MaRDI QIDQ18672FDOQ18672
Author name not available (Why is that?)
Official website: http://www.cl.cam.ac.uk/~jrh13/hol-light/
Cited In (only showing first 100 items - show all)
- Extending Sledgehammer with SMT solvers
- Certification of bounds on expressions involving rounded operators
- A Brief Overview of Mizar
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- BIGEBRA
- HOL-Boogie
- LEO-II
- Title not available (Why is that?)
- Theorema
- ML
- TPS
- Prosper
- MPTP 0.2
- Algolib
- Isar
- MetaPRL
- MoMM
- Mizar
- Why3
- QSopt_ex
- cvc3
- Gappa
- SPASS+T
- Proof General
- Isabelle/ZF
- zChaff
- z3
- HOL
- SLEEF
- CIRC
- Matita
- ETPS
- ProofPower
- OCaml
- Isabelle/jEdit
- PIDE
- HOL-Omega
- C-CoRN
- Flocq
- Nuprl
- SCOTT
- Satallax
- MML
- Hets
- Automath
- Kodkod
- dReal
- Sledgehammer
- MMT
- Twelf
- OMDoc
- Isabelle/PIDE
- QMT
- Lurch
- MaLeCoP
- MathDox
- veriT
- NQTHM
- CVC Lite
- Polar
- MaSh
- MathXpert
- LCF
- OpenSMT
- CakeML
- NLCertify
- Robotica
- IMPS
- Coq/SSReflect
- MetaOCaml
- FABRIK
- Lem
- Agda
- gaia
- Cayenne
- CompCert
- ForTheL
- CondLean
- CSLLean
- Dr.Doodle
- Squolem
- JProver
- KLMLean
- Milawa
- QMLTP
- TLAPS
- PhoX
- Gandalf
- NESCOND
- E Theorem Prover
- Flyspeck
- Ivy
- PRocH
- MaLARea
- MizAR 40 for Mizar 40
- Analytic tableaux for higher-order logic with choice
- FoCaLiZe and Dedukti to the rescue for proof interoperability
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- Metis
- Coquelicot: a user-friendly library of real analysis for Coq
This page was built for software: HOL Light
