GeoCoq

Michael Beeson; Pierre Boutry; Gabriel Braun; Charly Gries; Julien Narboux

Logiciel Année : 2018

GeoCoq

(1) , (2) , (2) , (2) , (2)

1
2

Michael Beeson

Fonction : Auteur
PersonId : 960560

San Jose State University [San Jose]

Pierre Boutry

Fonction : Auteur
PersonId : 2808
IdHAL : boutry

Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie

Gabriel Braun

Fonction : Auteur

Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie

Charly Gries

Fonction : Auteur
PersonId : 972908

Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie

Julien Narboux

Fonction : Auteur
PersonId : 4534
IdHAL : julien-narboux
ORCID : 0000-0003-3527-7184
IdRef : 111206480

Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie

Résumé

A formalization of geometry in Coq. This library contains a formalization of geometry using the Coq proof assistant. It contains both proofs about the foundations of geometry and high-level proofs in the same style as in high-school.

Mots clés

coordinates Triangle centers parallel postulates Euclidean geometry Formal proofs Coq Proof Assistant Foundations of geometry arithmetization Thales theorem pythagoras theorem neutral geometry Tarski's geometry Hilbert's geometry