Tuan-Minh Pham, Yves Bertot, Julien Narboux. A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry. In Beniamino Murgante, Osvaldo Gervasi, Andrés Iglesias, David Taniar, Bernady O. Apduhan, editors, Computational Science and Its Applications - ICCSA 2011 - International Conference, Santander, Spain, June 20-23, 2011. Proceedings, Part IV. Volume 6785 of Lecture Notes in Computer Science, pages 368-383, Springer, 2011. [doi]
Abstract is missing.