HOL Light

swMATH6580MaRDI QIDQ18672

No author found.

Related Items (only showing first 100 items - show all)

A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving ⋮ Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17--21, 2017. Proceedings ⋮ Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm ⋮ Formal verification of stability and chaos in periodic optical systems ⋮ An approximation framework for solvers and decision procedures ⋮ Theory morphisms in Church's type theory with quotation and evaluation ⋮ Semantic representation of general topology in the Wolfram language ⋮ A web-based toolkit for mathematical word processing applications with semantics ⋮ Formalization of transform methods using HOL Light ⋮ Classification of alignments between concepts of formal mathematical systems ⋮ versat: A Verified Modern SAT Solver ⋮ Formalization of linear space theory in the higher-order logic proving system ⋮ From informal to formal proofs in Euclidean geometry ⋮ Proof-checking Euclid ⋮ Automated reasoning. Third international joint conference, IJCAR 2006, Seattle, WA, USA, August 17--20, 2006. Proceedings ⋮ HOL Light: An Overview ⋮ Standalone Tactics Using OpenTheory ⋮ Unnamed Item ⋮ Verification of clock synchronization algorithms: experiments on a combination of deductive tools ⋮ Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22--26, 2013. Proceedings ⋮ Computer assisted reasoning. A Festschrift for Michael J. C. Gordon ⋮ Formalizing an analytic proof of the prime number theorem ⋮ Rewriting conversions implemented with continuations ⋮ Crystal: Integrating structured queries into a tactic language ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Verifying integer programming results ⋮ WorkflowFM: a logic-based framework for formal process specification and composition ⋮ Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge ⋮ Pascal's theorem in real projective plane ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Self-certification ⋮ Proof-Producing Reflection for HOL ⋮ A Consistent Foundation for Isabelle/HOL ⋮ Pattern Matches in HOL: ⋮ A modeling and verification framework for optical quantum circuits ⋮ Formalization of functional variation in HOL Light ⋮ Proof Assistants for Natural Language Semantics ⋮ Random Forests for Premise Selection ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving ⋮ Friends with Benefits ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ Certification of bounds on expressions involving rounded operators ⋮ Lem ⋮ Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving ⋮ Unnamed Item ⋮ Error analysis of digital filters using HOL theorem proving ⋮ Unnamed Item ⋮ The Coq library as a theory graph ⋮ Inspection and selection of representations ⋮ Witnessing (Co)datatypes ⋮ A parameterized floating-point formalizaton in HOL Light ⋮ Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics ⋮ Proving Valid Quantified Boolean Formulas in HOL Light ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism ⋮ Mechanised Computability Theory ⋮ Lem: A Lightweight Tool for Heavyweight Semantics ⋮ Composable Discovery Engines for Interactive Theorem Proving ⋮ GRUNGE: a grand unified ATP challenge ⋮ A formal proof of Pick's Theorem ⋮ HOL Zero’s Solutions for Pollack-Inconsistency ⋮ From Types to Sets by Local Type Definitions in Higher-Order Logic ⋮ Formalization of the Resolution Calculus for First-Order Logic ⋮ On the Formalization of Fourier Transform in Higher-order Logic ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time ⋮ A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs ⋮ Mechanized metatheory revisited ⋮ Formalization of geometric algebra in HOL Light ⋮ Automated Reasoning Service for HOL Light ⋮ Formal Mathematics on Display: A Wiki for Flyspeck ⋮ Capturing Hiproofs in HOL Light ⋮ On the Formal Analysis of Geometrical Optics in HOL ⋮ Developments in Formal Proofs ⋮ Certified Roundoff Error Bounds Using Semidefinite Programming ⋮ Lemma Mining over HOL Light ⋮ Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light ⋮ A Meta Linear Logical Framework ⋮ Extending Sledgehammer with SMT solvers ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13--17, 2015, Proceedings ⋮ Premise selection for mathematics by corpus analysis and kernel methods ⋮ On the formalization of gamma function in HOL ⋮ Proof-producing translation of higher-order logic into pure and stateful ML ⋮ Flyspecking Flyspeck ⋮ Towards a Formally Verified Proof Assistant ⋮ Implicational Rewriting Tactics in HOL ⋮ A Heuristic Prover for Real Inequalities ⋮ Cardinals in Isabelle/HOL ⋮ A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) ⋮ HOL with Definitions: Semantics, Soundness, and a Verified Implementation ⋮ Formal Verification of Optical Quantum Flip Gate

This page was built for software: HOL Light