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:

  • methods of automated deduction applied to checking students' input;
  • methods of automated deduction applied to prove post-conditions for particular problem solutions;
  • combinations of deduction and computation enabling systems to propose next steps;
  • automated provers specific for dynamic geometry systems;
  • proof and proving in mathematics education.

Invited Speaker

Julien Narboux

Julien Narboux, University of Strasbourg, France

GeoCoq: formalized foundations of geometry

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.