Pages that link to "Item:Q1945903"
From MaRDI portal
The following pages link to The HOL Light theory of Euclidean space (Q1945903):
Displaying 41 items.
- On the formal analysis of Gaussian optical systems in HOL (Q315313) (← links)
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (Q333325) (← links)
- A certified proof of the Cartan fixed point theorems (Q438546) (← links)
- A formalization of metric spaces in HOL Light (Q682381) (← links)
- Formalization of camera pose estimation algorithm based on Rodrigues formula (Q826358) (← links)
- Formal analysis of continuous-time systems using Fourier transform (Q1640640) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Formal kinematic analysis of a general 6R manipulator using the screw theory (Q1665987) (← links)
- Formalizing basic quaternionic analysis (Q1687738) (← links)
- The flow of ODEs: formalization of variational equation and Poincaré map (Q1722644) (← links)
- From types to sets by local type definition in higher-order logic (Q1722645) (← links)
- A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (Q1984794) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- Formalization of Euler-Lagrange equation set based on variational calculus in HOL light (Q2031406) (← links)
- A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
- Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← links)
- Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light} (Q2198134) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- An Isabelle/HOL formalisation of Green's theorem (Q2323451) (← links)
- Formalization of geometric algebra in HOL Light (Q2323452) (← links)
- On the formalization of gamma function in HOL (Q2352499) (← links)
- Formalizing complex plane geometry (Q2354913) (← links)
- Higher-order logic formalization of conformal geometric algebra and its application in verifying a robotic manipulation algorithm (Q2360828) (← links)
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem (Q2362109) (← links)
- Formalization of functional variation in HOL Light (Q2423767) (← links)
- A Formal Proof of Cauchy’s Residue Theorem (Q2829261) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- Formalization and Execution of Linear Algebra: From Theorems to Algorithms (Q3453644) (← links)
- Formalizing the Face Lattice of Polyhedra (Q5049001) (← links)
- (Q5094138) (← links)
- Pollack-inconsistency (Q5170237) (← links)
- On the Formalization of Cardinal Points of Optical Systems (Q5348536) (← links)
- Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm (Q5371950) (← links)
- Formalization of Complex Vectors in Higher-Order Logic (Q5495918) (← links)
- Matching Concepts across HOL Libraries (Q5495929) (← links)
- (Q5875423) (← links)
- A formalization of convex polyhedra based on the simplex method (Q5915783) (← links)
- Measure construction by extension in dependent type theory with application to integration (Q6050768) (← links)
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting (Q6108811) (← links)
- Formalization of the inverse kinematics of three-fingered dexterous hand (Q6156933) (← links)
- Formalizing Pick's theorem in Isabelle/HOL (Q6648161) (← links)