Cited in
(only showing first 100 items - show all)- Towards Self-verification of HOL Light
- Proof assistant decision procedures for formalizing origami
- Comprehending Isabelle/HOL’s Consistency
- Rigorous floating-point mixed-precision tuning
- Proof-producing reflection for HOL. With an application to model polymorphism
- Logic for programming, artificial intelligence, and reasoning. 20th international conference, LPAR-20 2015, Suva, Fiji, November 24--28, 2015. Proceedings
- Formalization of camera pose estimation algorithm based on Rodrigues formula
- A formalized proof of Dirichlet's theorem on primes in arithmetic progression
- An abstract interpretation framework for the round-off error analysis of floating-point programs
- On the Formal Analysis of Geometrical Optics in HOL
- A logical framework combining model and proof theory
- A formalization of metric spaces in HOL Light
- From types to sets by local type definition in higher-order logic
- Formal verification of stability and chaos in periodic optical systems
- Formal Proofs for Nonlinear Optimization
- The future of logic: foundation-independence
- Cardinals in Isabelle/HOL
- Importing HOL Light into Coq
- Building Formal Method Tools in the Isabelle/Isar Framework
- Extending Sledgehammer with SMT solvers
- A formalization of the Smith normal form in higher-order logic
- JEFL: joint embedding of formal proof libraries
- Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
- On duplication in mathematical repositories
- Scalable fine-grained proofs for formula processing
- Certification of nonclausal connection tableaux proofs
- From types to sets by local type definitions in higher-order logic
- A web-based toolkit for mathematical word processing applications with semantics
- Metamath Zero: designing a theorem prover prover
- WorkflowFM: a logic-based framework for formal process specification and composition
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Formalizing ordinal partition relations using Isabelle/HOL
- scientific article; zbMATH DE number 1949625 (Why is no real title available?)
- Towards Knowledge Management for HOL Light
- Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq
- Pattern matches in HOL: a new representation and improved code generation
- Representing model theory in a type-theoretical logical framework
- Lem: reusable engineering of real-world semantics
- A condensed semantics for qualitative spatial reasoning about oriented straight line segments
- Twenty Years of Theorem Proving for HOLs Past, Present and Future
- Certification of bounds on expressions involving rounded operators
- Proof-checking Euclid
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Extensional higher-order paramodulation in Leo-III
- The Imandra Automated Reasoning System (System Description)
- Lemma Mining over HOL Light
- A Brief Overview of Mizar
- Mechanized metatheory revisited
- Deductive verification of floating-point Java programs in KeY
- Automating theorem proving with SMT
- Aligning concepts across proof assistant libraries
- Real Number Calculations and Theorem Proving
- Witnessing (co)datatypes
- scientific article; zbMATH DE number 5850137 (Why is no real title available?)
- An experiment concerning mathematical proofs on computers with French undergraduate students
- Formal proofs of hypergeometric sums. Dedicated to the memory of Andrzej Trybulec
- A heuristic prover for real inequalities
- On definitions of constants and types in HOL
- The higher-order prover \textsc{Leo}-II
- Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
- Formalization of complex vectors in higher-order logic
- scientific article; zbMATH DE number 1863397 (Why is no real title available?)
- Combining Decision Procedures by (Model-)Equality Propagation
- A heuristic prover for real inequalities
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Theorem proving in higher order logics. 14th international conference, TPHOLs 2001, Edinburgh, Scotland, GB, September 3--6, 2001. Proceedings
- Formalization of complex analysis and matrix theory
- A Compressing Translation from Propositional Resolution to Natural Deduction
- Formalizing geometric algebra in Lean
- Formalizing an analytic proof of the prime number theorem
- Incorporating quotation and evaluation into Church's type theory
- Combining decision procedures by (model-)equality propagation
- A certified proof of the Cartan fixed point theorems
- Monotonicity inference for higher-order formulas
- Theorem Proving in Higher Order Logics
- Sharing HOL4 and HOL Light proof knowledge
- Random forests for premise selection
- Developments in formal proofs
- Mechanizing metatheory in a logical framework
- Certified roundoff error bounds using semidefinite programming
- Deciding floating-point logic with abstract conflict driven clause learning
- Matching concepts across HOL libraries
- Towards the formalization of fractional calculus in higher-order logic
- Steps towards Verified Implementations of HOL Light
- Proof assistants for natural language semantics
- FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
- A formal proof of the Kepler conjecture
- A parameterized floating-point formalizaton in HOL Light
- Automated Deduction – CADE-20
- A verified proof checker for higher-order logic
- Incorporating quotation and evaluation into Church's type theory: syntax and semantics
- Conversion of HOL Light proofs into Metamath
- From informal to formal proofs in Euclidean geometry
- Formal Methods in Computer-Aided Design
- Fast LCF-Style Proof Reconstruction for Z3
- Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7--11, 2014. Proceedings
- Automating Elementary Number-Theoretic Proofs Using Gröbner Bases
- Formal analysis of continuous-time systems using Fourier transform
- The role of entropy in guiding a connection prover
This page was built for software: HOL Light
