HOL

swMATH5492MaRDI QIDQ17631

No author found.

Described by source

• A Brief Overview of HOL4

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

Automatic Proof and Disproof in Isabelle/HOL ⋮ Formalization of Finite-State Discrete-Time Markov Chains in HOL ⋮ Towards Formal Fault Tree Analysis Using Theorem Proving ⋮ Formal Logic Definitions for Interchange Languages ⋮ Formalizing Physics: Automation, Presentation and Foundation Issues ⋮ Combining Model Checking and Deduction ⋮ Symbolic Trajectory Evaluation ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 ⋮ Formal verification of standards for distance vector routing protocols ⋮ AUSPICE-R: Automatic Safety-Property Proofs for Realistic Features in Machine Code ⋮ Relation-Algebraic Verification of Prim’s Minimum Spanning Tree Algorithm ⋮ Specifying Properties of Dynamic Architectures Using Configuration Traces ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Sharing HOL4 and HOL Light Proof Knowledge ⋮ Without Loss of Generality ⋮ HOL Light: An Overview ⋮ Formal Analysis of Optical Waveguides in HOL ⋮ The HOL-Omega Logic ⋮ A Purely Definitional Universal Domain ⋮ Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL ⋮ Tool-Based Verification of a Relational Vertex Coloring Program ⋮ Standalone Tactics Using OpenTheory ⋮ An Axiomatization for Cylinder Computation Model ⋮ Unified Classical Logic Completeness ⋮ Type Theory and Formal Proof ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Aliasing Restrictions of C11 Formalized in Coq ⋮ Nonfree Datatypes in Isabelle/HOL ⋮ Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL ⋮ Certified Kruskal’s Tree Theorem ⋮ Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties ⋮ A Formal Model and Correctness Proof for an Access Control Policy Framework ⋮ Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems ⋮ Proof-Producing Reflection for HOL ⋮ Improved Tool Support for Machine-Code Decompilation in HOL4 ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ A Verified Enclosure for the Lorenz Attractor (Rough Diamond) ⋮ A Consistent Foundation for Isabelle/HOL ⋮ Refinement to Imperative/HOL ⋮ Amortized Complexity Verified ⋮ Deriving Comparators and Show Functions in Isabelle/HOL ⋮ Formalising Knot Theory in Isabelle/HOL ⋮ Pattern Matches in HOL: ⋮ Hoare Logic for ARM Machine Code ⋮ Proofs and Reconstructions ⋮ An Axiomatic Value Model for Isabelle/UTP ⋮ A Modular Formalisation of Finite Group Theory ⋮ Verification of Expectation Properties for Discrete Random Variables in HOL ⋮ Automatically Translating Type and Function Definitions from HOL to ACL2 ⋮ HOL2P - A System of Classical Higher Order Logic with Second Order Polymorphism ⋮ Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving ⋮ Unnamed Item ⋮ Friends with Benefits ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) ⋮ Twenty Years of Theorem Proving for HOLs Past, Present and Future ⋮ The Isabelle Framework ⋮ A Compiled Implementation of Normalization by Evaluation ⋮ LCF-Style Propositional Simplification with BDDs and SAT Solvers ⋮ Formal Reasoning About Causality Analysis ⋮ Proof Pearl: Revisiting the Mini-rubik in Coq ⋮ Concept Formation via Proof Planning Failure ⋮ A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems ⋮ Machine-Checked Proof-Theory for Propositional Modal Logics ⋮ Fixpoints and Search in PVS ⋮ A Formal Quantifier Elimination for Algebraically Closed Fields ⋮ A Formalisation of the Normal Forms of Context-Free Grammars in HOL4 ⋮ Unnamed Item ⋮ Unifying Theories in Isabelle/HOL ⋮ Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays ⋮ Unifying Sets and Programs via Dependent Types ⋮ Formalization of Continuous Probability Distributions ⋮ Using the TPTP Language for Writing Derivations and Finite Interpretations ⋮ Towards Self-verification of HOL Light ⋮ Verified Synthesis of Knowledge-Based Programs in Finite Synchronous Environments ⋮ Three Chapters of Measure Theory in Isabelle/HOL ⋮ Termination of Isabelle Functions via Termination of Rewriting ⋮ Validating QBF Validity in HOL4 ⋮ Animating the Formalised Semantics of a Java-Like Language ⋮ Formalization of Entropy Measures in HOL ⋮ A Verified Runtime for a Verified Theorem Prover ⋮ Mechanised Computability Theory ⋮ seL4 Enforces Integrity ⋮ LCF-Style Bit-Blasting in HOL4 ⋮ Lem: A Lightweight Tool for Heavyweight Semantics ⋮ Heterogeneous Proofs: Spider Diagrams Meet Higher-Order Provers ⋮ Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL

This page was built for software: HOL