package coq-ruler-compass-geometry

  1. Overview
  2. No Docs
Ruler and compass geometry axiomatization

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. J
    Jean Duprat <Jean.Duprat@ens-lyon.fr>

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.10.0.tar.gz
md5=3d5695aff6d8315854abfe92593a744b

Description

This library contains an axiomatization of the ruler and compass euclidian geometry. Files A1 to A6 contain the axioms and the basic constructions. The other files build the proof that this axiomatization induces the whole plane geometry except the continuity axiom. For that the proofs of the Hilbert's axioms conclude this work in the files E1 to E5.

Tags

keyword: geometry keyword: plane geometry keyword: ruler and compass geometry keyword: Euclidian geometry keyword: Hilbert's axioms category: Mathematics/Geometry/General date: 2007-11

Published: 07 Dec 2019

Dependencies (2)

  1. coq >= "8.10" & < "8.11~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None