Formalization of camera pose estimation algorithm based on Rodrigues formula

DOI10.1007/s00165-020-00520-5zbMath1458.68226OpenAlexW3094766313MaRDI QIDQ826358

Qianying Zhang, Ximeng Li, Shanyan Chen, Yong Guan, Zhiping Shi, Guo-hui Wang

Publication date: 4 January 2021

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-020-00520-5

zbMATH Keywords

Rodrigues formulaleast squares methodHOL Lightformalizationcamera pose estimation

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Machine vision and scene understanding (68T45) Artificial intelligence for robotics (68T40) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Verified interactive computation of definite integrals

Uses Software

• HOL Light
• GitHub
• EPnP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A novel solution to the P4P problem for an uncalibrated camera
• A compact formula for rotations as spin matrix polynomials
• Principal rotation representations of proper \(N\times N\) orthogonal matrices
• Modified Rodrigues parameters: an efficient representation of orientation in 3D vision and graphics
• The HOL Light theory of Euclidean space
• A novel linear algorithm for \(P5P\) problem

This page was built for publication: Formalization of camera pose estimation algorithm based on Rodrigues formula