Theorem Proving in Higher Order Logics
From MaRDI portal
Publication:5477650
DOI10.1007/11541868zbMath1152.68520OpenAlexW2484880499MaRDI QIDQ5477650
No author found.
Publication date: 6 July 2006
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11541868
Related Items (35)
A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Formal analysis of the kinematic Jacobian in screw theory ⋮ Formal verification of C systems code. Structured types, separation logic and theorem proving ⋮ Readable Formalization of Euler’s Partition Theorem in Mizar ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Flyspeck II: The basic linear programs ⋮ Without Loss of Generality ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Formalizing an analytic proof of the prime number theorem ⋮ A verified ODE solver and the Lorenz attractor ⋮ A Formalized Hierarchy of Probabilistic System Types ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ Formalizing basic quaternionic analysis ⋮ Formalising Mathematics in Simple Type Theory ⋮ The HOL Light theory of Euclidean space ⋮ Towards a UTP Semantics for Modelica ⋮ A certified proof of the Cartan fixed point theorems ⋮ Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm ⋮ The flow of ODEs: formalization of variational equation and Poincaré map ⋮ From types to sets by local type definition in higher-order logic ⋮ Canonical Big Operators ⋮ Formal analysis of optical systems ⋮ A formalization of metric spaces in HOL Light ⋮ A revision of the proof of the Kepler conjecture ⋮ A formal proof of the expressiveness of deep learning ⋮ A formal proof of the expressiveness of deep learning ⋮ A verified generational garbage collector for CakeML ⋮ Formalization of function matrix theory in HOL ⋮ Point-Free, Set-Free Concrete Linear Algebra ⋮ Three Chapters of Measure Theory in Isabelle/HOL ⋮ LCF-Style Bit-Blasting in HOL4 ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ Coquet: A Coq Library for Verifying Hardware ⋮ Formalization of geometric algebra in HOL Light ⋮ Formalizing complex plane geometry
Uses Software
This page was built for publication: Theorem Proving in Higher Order Logics
