HOL Light
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Towards finding longer proofs
- Refactoring proofs with Tactician
- Error analysis of digital filters using HOL theorem proving
- A formalization of the LLL basis reduction algorithm
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
- Machine learning guidance for connection tableaux
- TacticToe: learning to prove with tactics
- Efficient formal verification of bounds of linear programs
- Partial Recursive Functions in Higher-Order Logic
- Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17--21, 2017. Proceedings
- Formalization of linear space theory in the higher-order logic proving system
- Generic literals
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Efficiently checking propositional refutations in HOL theorem provers
- Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application
- Classification of alignments between concepts of formal mathematical systems
- scientific article; zbMATH DE number 1614683 (Why is no real title available?)
- On the formal analysis of Gaussian optical systems in HOL
- Formalization of Laplace transform using the multivariable calculus theory of HOL-Light
- Semantic representation of general topology in the Wolfram language
- On the formalization of Fourier transform in higher-order logic
- scientific article; zbMATH DE number 7106480 (Why is no real title available?)
- Theory morphisms in Church's type theory with quotation and evaluation
- Rocket-Fast Proof Checking for SMT Solvers
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- Formal analysis of optical systems
- Enabling symbolic and numerical computations in HOL Light
- A Skeptic's approach to combining HOL and Maple
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11--14, 2010. Proceedings
- ACETAF
- Apron
- ACL2
- BIGEBRA
- Coq
- HOL-Boogie
- Isabelle
- LEO-II
- MetiTarski
- scientific article; zbMATH DE number 1670746 (Why is no real title available?)
- 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
This page was built for software: HOL Light
