A case study in formalizing projective geometry in Coq: Desargues theorem.

Nicolas Magaud Julien Narboux Pascal Schreck

Published in: Comput. Geom. (2012)

Keyphrases

projective geometry
cross ratio
computer vision
camera calibration
camera parameters
fractional programming
three dimensional
image planes
pose estimation
straight line
real time
digital images
low cost
lens distortion