Skip to main content
PRL Project

Building Mathematics-Based Software Systems to Advance Science and Create Knowledge

by Robert L. Constable

Appears in Efficient Algorithms: Essays Dedicated to Kurt Mehlhorn on the Occasion of His 60th Birthday from Springer, 2009.

Kurt Mehlhorn's foundational results in computational geometry provide not only a basis for practical geometry systems such as Leda and CGAL, they also, in the spirit of Euclid, provide a sound basis for geometric truth. This article shows how Mehlhorn's ideas from computational geometry have influenced work on the logical basis for constructive geometry. In particular there is a sketch of new decidability results for constructive Euclidean geometry as formulated in computational type theory, CTT. Theorem proving systems for type theory are important in establishing knowledge to the highest standards of certainty, and in due course they will play a significant role in geometry systems.

bibTex ref: Con09

cite link