The HOL Light theory of Euclidean space

DOI10.1007/S10817-012-9250-9zbMath1260.68373OpenAlexW2091456056MaRDI QIDQ1945903

Yanyan Li

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

zbMATH Keywords

Euclidean spacevector spaceformalized mathematics\texttt{HOL Light}

Mathematics Subject Classification ID

Related Items (38)

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

• Coq
• Mizar
• HOL Light
• Sledgehammer
• Automath
• Gandalf
• Flyspeck
• Jordan
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A revision of the proof of the Kepler conjecture
• Without Loss of Generality
• Some Combinatorial Lemmas in Topology
• The Jordan Curve Theorem, Formally and Informally
• Theorem Proving in Higher Order Logics
• Importing HOL Light into Coq

This page was built for publication: The HOL Light theory of Euclidean space