Zajednički sastanak ARGO seminara i seminara Katedre za računarstvo i informatiku, 23. mart 2017.

• 23. Mart,  2017
• Komentari (0)

Zajednički sastank ARGO seminara i seminara Katedre za računarstvo i informatiku biće održan u četvrtak, 23. marta 2017. u sali 718 Matematičkog fakulteta sa početkom u 18:15 časova.

Predavač: Julien Narboux, Univerzitet u Strazburu

Naslov predavanja: GeoCoq, FOUNDATIONS OF GEOMETRY FORMALIZED IN Coq

Apstrakt: 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.

---