Workshop at FLOC 2018, Oxford, UK, 18 July 2018 (Post-FLoC workshop)
(Computer) Theorem Proving (TP) is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brings together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems. Topics of interest include:
Julien Narboux, University of Strasbourg, France
Geometry is central in both the history and teaching of the structure of mathematical proofs and the axiomatic method.
In this talk, we will give an overview of the GeoCoq library. The library developed in collaboration with P.Boutry, G. Braun, C. Gries and P. Schreck consists in a formalization of geometry using the Coq proof assistant.
Starting from the foundations based on either Euclid’s, Tarski’s, or Hilbert’s axiom systems, we formalized the traditional results which can be used for high-school exercises.
We will discuss the axiomatizations and the automation necessary for use in the classroom.
Based on some examples taken from highschool exercices, we will revisit some traditional proofs from a formal point of view.