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
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
