The HOL Light theory of Euclidean space
From MaRDI portal
Publication:1945903
DOI10.1007/s10817-012-9250-9zbMath1260.68373OpenAlexW2091456056MaRDI QIDQ1945903
Publication date: 17 April 2013
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-012-9250-9
Related Items
Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm, A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem, Formalization of camera pose estimation algorithm based on Rodrigues formula, Formalizing the Face Lattice of Polyhedra, Formalization and Execution of Linear Algebra: From Theorems to Algorithms, On the formal analysis of Gaussian optical systems in HOL, Formal analysis of continuous-time systems using Fourier transform, Aligning concepts across proof assistant libraries, Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL, Program logic for higher-order probabilistic programs in Isabelle/HOL, Formal kinematic analysis of a general 6R manipulator using the screw theory, On the Formalization of Cardinal Points of Optical Systems, Measure construction by extension in dependent type theory with application to integration, A Formal Proof of the Computation of Hermite Normal Form in a General Setting, Formalization of functional variation in HOL Light, Formalization of the inverse kinematics of three-fingered dexterous hand, Unnamed Item, Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light}, A Coq formalization of Lebesgue induction principle and Tonelli's theorem, Formalization of real analysis: a survey of proof assistants and libraries, Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm, Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL, The flow of ODEs: formalization of variational equation and Poincaré map, From types to sets by local type definition in higher-order logic, A verified implementation of the Berlekamp-Zassenhaus factorization algorithm, Pollack-inconsistency, Coquelicot: a user-friendly library of real analysis for Coq, A formalization of convex polyhedra based on the simplex method, Unnamed Item, Formalization of Euler-Lagrange equation set based on variational calculus in HOL light, A Formal Proof of Cauchy’s Residue Theorem, An Isabelle/HOL formalisation of Green's theorem, Formalization of geometric algebra in HOL Light, Formalization of Complex Vectors in Higher-Order Logic, Matching Concepts across HOL Libraries, A formalization of the Smith normal form in higher-order logic, On the formalization of gamma function in HOL, Formalizing complex plane geometry
Uses Software
Cites Work
