Skip to main content
PRL Project

A formal exploration of constructive geometry
Main page

Previous Page


  1. Avigad, J., E. Dean. and J. Mumma. A formal system for Euclid’s Elements. Review of Symbolic Logic, 2(4): 700-768. 2009.

  2. Beeson, Michael . A constructive version of Tarski's geometry. Annals of Pure and Applied Logic, 166(11): 1199-1273. 2015.

  3. Beeson, Michael . Proof and computation in geometry. In International Workshop on Automated Deduction in Geometry. Springer Berlin Heidelberg, 2012.

  4. Beeson, Michael . Constructive geometry. In Proceedings of the Tenth Asian Logic Colloquium, Kobe, Japan. 2010.

  5. Beeson, Michael . Foundations of Constructive Euclidean Geometry. 2009.

  6. Heath, Thomas Little, ed. The thirteen books of Euclid's Elements. Courier Corporation, 1956.

  7. Hilbert, David. The foundations of geometry. Open court publishing Company, 1902.

  8. Proclus. Proclus, A Commentary on the First Book of Euclid's Elements, translated by Glenn R. Morrow. (Princeton 1970).

  9. Tarski, Alfred. What is elementary geometry?. Studies in Logic and the Foundations of Mathematics 27 (1959): 16-29.

  10. Tarski, Alfred and Givant, Steven. Tarski's System of Geometry. The Bulletin of Symbolic Logic 5, no. 2 (1999): 175-214.

    The interactive diagrams were drawn using the Javascript library JSXGraph.

Previous Page


Website feedback
PRL Project   |   Computer Science Department   |   Cornell University   |   320 Gates Hall, Ithaca, NY 14853   |   © 2014 Cornell University
site admin | Prof Constable's Library | PRL SourceForge Project Page