Заједнички састанак АРГО семинара и семинара Катедре за рачунарство и информатику, 23. март 2017.

Заједнички састанк АРГО семинара и семинара Катедре за рачунарство и информатику биће одржан у четвртак, 23. марта 2017. у сали 718 Математичког факултета са почетком у 18:15 часова.

Предавач: Julien Narboux, Универзитет у Стразбуру

Наслов предавања: GeoCoq, FOUNDATIONS OF GEOMETRY FORMALIZED IN Coq

Апстракт:  In this talk we will give an overview of the GeoCoq library developed by our team in Strasbourg (http://geocoq.github.io/GeoCoq/). GeoCoq library contains a systematic development of geometry from Tarski’s or Hilbert’s axioms. From these axiom systems, we formalized the culminating results of both Tarski, Schwabhäuser, Szmielew, Metamathematische Methoden in der Geometrie and Hilbert, Foundations of Geometry, namely the arithmetization of geometry. This connection between synthetic geometry and algebra, allows us to use algebraic methods for automated deduction in geometry in a synthetic setting. We have also studied the formal proof of the equivalence between 34 versions of the parallel postulates. We work in neutral geometry in an intuitionistic setting and study the impact of different continuity properties on the equivalence proofs. This result in four groups of postulates, which are all equivalent assuming Archimedes’ axiom but distinct, in constructive logic without Archimedes’ axiom. Finally, I will report our ongoing work toward the formalization of Euclid’s Elements proposition in Coq.