HOL Light

swMATH6580MaRDI QIDQ18672FDOQ18672

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• On the Formal Analysis of Geometrical Optics in HOL
• The future of logic: foundation-independence
• 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
• Towards Knowledge Management for HOL Light
• Lem: reusable engineering of real-world semantics
• Representing model theory in a type-theoretical logical framework
• Certification of bounds on expressions involving rounded operators
• Theorem Proving in Large Formal Mathematics as an Emerging AI Field
• A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs
• A synthesis of the procedural and declarative styles of interactive theorem proving
• A Brief Overview of Mizar
• Friends with Benefits
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The Lean Theorem Prover (System Description)
• THF0 – The Core of the TPTP Language for Higher-Order Logic
• 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
• Mechanizing metatheory in a logical framework
• MaSh: Machine Learning for Sledgehammer
• Steps towards Verified Implementations of HOL Light
• Automated Deduction – CADE-20
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• Deciding floating-point logic with abstract conflict driven clause learning
• An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
• Fast LCF-Style Proof Reconstruction for Z3
• Efficiently checking propositional refutations in HOL theorem provers
• On the formal analysis of Gaussian optical systems in HOL
• On the Formalization of Cardinal Points of Optical Systems
• Formal analysis of optical systems
• A Skeptic's approach to combining HOL and Maple
• TacticToe: Learning to Reason with HOL4 Tactics
• PRocH: Proof Reconstruction for HOL Light
• A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
• Title not available (Why is that?)
• Extending Sledgehammer with SMT Solvers
• VeriML
• MizAR 40 for Mizar 40
• A learning-based fact selector for Isabelle/HOL
• Floating-point arithmetic on the test bench. How are verified numerical solutions calculated?
• Flexary connectives in Mizar
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• HOL Light QE
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• Communicating Formal Proofs: The Case of Flyspeck
• Analytic tableaux for higher-order logic with choice
• Theorem Proving in Higher Order Logics
• Automated deduction -- CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9--14, 2013. Proceedings
• HOL(y)Hammer: online ATP service for HOL Light
• Efficient and accurate computation of upper bounds of approximation errors
• Isabelle's metalogic: formalization and proof checker
• The Isabelle/Naproche natural language proof assistant
• Extending Sledgehammer with SMT solvers
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• On the formalization of gamma function in HOL
• Premise selection for mathematics by corpus analysis and kernel methods
• Formalization of real analysis: a survey of proof assistants and libraries
• Generic Literals
• The HOL Light theory of Euclidean space
• Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings
• Preface
• Automated Reasoning Service for HOL Light
• Proof-producing translation of higher-order logic into pure and stateful ML
• A Heuristic Prover for Real Inequalities
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• Towards a Formally Verified Proof Assistant
• FoCaLiZe and Dedukti to the rescue for proof interoperability
• Formalization of geometric algebra theories in higher-order logic
• A Verified Runtime for a Verified Theorem Prover
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
• Hammer for Coq: automation for dependent type theory
• HOL Light: An Overview
• Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials
• Coquelicot: a user-friendly library of real analysis for Coq
• A Declarative Language for the Coq Proof Assistant
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Canonical Big Operators
• Proving Bounds on Real-Valued Functions with Computations
• Towards Self-verification of HOL Light
• Formal Proofs for Nonlinear Optimization
• Formal Mathematics on Display: A Wiki for Flyspeck
• Cardinals in Isabelle/HOL
• From types to sets by local type definition in higher-order logic
• Efficient Formal Verification of Bounds of Linear Programs
• Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving
• Title not available (Why is that?)
• Mechanized metatheory revisited
• Views of Pi: definition and computation
• Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics
• Real Number Calculations and Theorem Proving
• A Consistent Foundation for Isabelle/HOL

This page was built for software: HOL Light