This
program is an interactive geometry software with proof related features.
The project consist in producing an interactive proof software for
geometry.
GeoProof can communicate with the Coq proof assistant to perform automatic and interactive proofs of geometry theorems.
GeoProof can communicate with CoqIde (a user interface for Coq). The
user can build a construction using GeoProof and the corresponding
formula is automatically translated into Coq's syntax.
Detailed
feature list :
five types of
geometric objects : points, lines, circles, vectors and segments
three
transformations : central symmetry, translation, and axial symmetry
- nine ways to build a point :
free point
point on circle
point on line
point on segment
point on half
plane
midpoint
point at
intersection of
two lines
one line and one circle
two circles
five ways to build a line
line passing by two points
perpendicular line
parallel line
perpendicular bisector
angle bisector
three ways to build a circle
by center and a point
using a diameter
by three points
text labels with dynamic
parts which can be the following :
measures :
distances
angles
areas
property
tests :
collinearity
point equality
orthogonality
parallelism
betweeness
congruence of angles
congruence of distances
left-turn
let x = ... in
formulas using + - * /
sin, cos, tan, arccos, arcsin, arctan, min, max...
