## TalksAll the slides linked here are PDF files. Although your browser may be able to display a PDF, generally they will look better if you open them in Adobe Reader. Therefore, rather than just clicking the links to the slides, you may want to right-click it and download, then double-click the downloaded file to open it in Adobe Reader. Once you open the PDF file in Adobe Reader, choose View | Full Screen, and then press Enter to advance to the next slidex. ## Proof-checking Euclid I gave this one-hour talk several times: - logic seminar in Munich (October 11, 2017)
- logic seminar in Utrecht (October 25, 2017)
- Institute for Cybernetics, Artificial Intelligence, and Robotics in Prague (November 2, 2017)
- Mathematics Colloquium at the University of Cairo (November 15, 2017)
- Colloquium of the Group on Logic, Methodology, and Philosophy of Sciences at the University of California, Berkeley (February 9, 2018)
- Mathematics Colloquium of the University of California, Santa Cruz (February 27, 2018).
## Tarskian Geometry and Ruler-and-compass constructionsI gave this one-hour talk at the Stanford Logic Seminar, April 15, 2014. ## Proof and Computation in GeometryI gave this 60-minute talk in Edinburgh, UK, September 19, 2012, at a conference on Automated Deduction in Geometry. ## Logic of Ruler and Compass ConstructionsI gave this fifteen-minute talk in Cambridge, England, June 19, 2012. ## Foundations of Constructive GeometryI gave this one-hour talk at the Stanford logic seminar, March 13, 2012; and essentially the same talk in Utrecht, June 11, 2012. ## Triangle TilingI gave this ten-minute talk at the AMS meeting in Boston, January, 2012. ## The Parallel Postulate in Constructive GeometryI gave this talk at the Symposium on Constructive Geometry, Stanford, October 24, 2009. For further background see the talk on Constructive Geometry linked below. ## Finiteness in Plateau's ProblemI gave this talk at the Bay Area Differential Geometry Seminar, Stanford, January 31, 2009. The last section was updated in 2015. ## Mathematical Logic and Computers: some interesting examplesI gave this talk in Kobe, Japan, on August 31, 2008. ## Constructive GeometryVersions of this talk were given in Leiden, January 2007, and in the Stanford Logic Seminar, February 2007. These slides are a long version, presenting the state of the work in August, 2008. A shortened version was given in Kobe, Japan, in September, 2008. ## The Meaning of ExistenceI gave this talk at a meeting of the MAA in August, 2007, in San José, California, and again at the Philosophy Department Colloquium in San José in March, 2009. ## The Mechanization of MathematicsI gave this talk at a meeting of the BAMA (Bay Area Mathematics Association) in October, 2005. ## Constructibility, Computability, and the Continuum.I gave this talk at the Stanford ASL meeting, March 2005. ## Implicit Typing in Lambda LogicI gave this talk at the ESHOL workshop of the Logic Programming and Automated Reasoning (LPAR-12) meeting in Jamaica, 2005. ## Automatic Derivation of the Equation of Motion of a PendulumI gave this talk at the Stanford Artificial Intelligence Seminar in April, 1987; and again at the UCSC math colloquium in May, 1987; but somehow never got around to publishing the work. Now the original computer program seems to be lost. |