HOL Light
From MaRDI portal
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
- ACETAF
- Apron
- ACL2
- BIGEBRA
- Coq
- HOL-Boogie
- Isabelle
- LEO-II
- MetiTarski
- Title not available (Why is that?)
- Nitpick
- PGB
- Proviola
- Theorema
- ML
- TPS
- Prosper
- Isabelle/HOL
- Isabelle/Isar
- IsaPlanner
- CAS/PI
- LINK
- MPTP
- MPTP 0.2
- HOL-Z
- VLISP
- VAMPIRE
- CoqEAL
- PVS
- MathWebSearch
- THF0
- Algolib
- gensim
- TPTP
- 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
- 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
