A Coq-Based Library for Interactive and Automated Theorem Proving in Plane Geometry.

Tuan-Minh Pham, Yves Bertot, Julien Narboux

Browse the full ICCSA paper archive.