A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton's Principia.

Jacques D. Fleuriot, Lawrence C. Paulson

Browse the full CADE paper archive.