The GeoProver Package for Mechanized (Plane) Geometry Theorem Proving
Version 1.3a

AUTHOR : Hans-Gert Graebe
ADDRESS : Univ. Leipzig, Institut f. Informatik, D - 04109 Leipzig, Germany
URL : http://www.informatik.uni-leipzig.de/~graebe

Introduction

The GeoProver is a small package for mechanized (plane) geometry manipulations with non degeneracy tracing, available for different CAS platforms (Maple, MuPAD, Mathematica, and Reduce).

It provides the casual user with a couple of procedures that allow him/her to mechanize his/her own geometry proofs. Version 1.1 grew out from a course of lectures for students of computer science on this topic held by the author at the Univ. of Leipzig in fall 1996 and was updated after a similar lecture in spring 1998.

The (completely revised) version 1.2, finished in March 2002, was set up as a generic software project to manage the code for different platforms in a unified way. There is a close relationship to the SymbolicData project (see http://www.symbolicdata.org).

For examples we refer to the test file, but also to the SymbolicData GEO collection. It contains many (generic) proof schemes of geometry theorems, mainly from Chou's book. These proof schemes can be translated to the GeoProver syntax for different platforms with SymbolicData tools.

For version 1.3 the syntax definition (the GeoCode) was separated from the GeoProver implementation. The latter is an implementation of the GeoCode standard using the coordinate method.

Note that function names change with different versions of the GeoCode standard. GeoProver 1.3 implements the GeoCode standard 1.3.

Please send comments, bug reports, hints, wishes, criticisms etc. to the author.

Basic Data Types

Basic data types are Points, Lines, and Circles.

A point A:=Point(a,b) represents a point with coordinates $(a1,a2)$ .

A line l:=Line(a,b,c) represents the line ${ (x,y) : a*x+b*y+c=0 }$ .

A circle c:=Circle(c1,c2,c3,c4) represents the circle ${ (x,y) : c1*(x^2+y^2)+c2*x+c3*y+c4=0 }$ .

Available functions

Point(a:Scalar, b:Scalar) Point constructor. Returns a coding for the point with coordinates (a,b).
altitude(A:Point, B:Point, C:Point) The altitude from $A$ onto $g(BC)$ .
angle_sum(a:Scalar, b:Scalar) Returns $tan(alpha+beta)$ , if $a=tan(alpha), b=tan(beta)$ .
centroid(A:Point, B:Point, C:Point) Centroid of the triangle $ABC$ .
circle_center(c:Circle) The center of the circle $c$ .
circle_slider(M:Point, A:Point, u:Scalar) Choose a point on the circle with center $M$ and point $A$ on the perimeter using a rational parametrization with parameter $u$ .
circle_sqradius(c:Circle) The squared radius of the circle $c$ .
circumcenter(A:Point, B:Point, C:Point) The circumcenter of the triangle $ABC$ .
csym_point(P:Point, Q:Point) The point symmetric to $P$ wrt. $Q$ as symmetry center.
eq_angle(A:Point, B:Point, C:Point, D:Point, E:Point, F:Point) Test for equal angle w(ABC) = w(DEF).
eq_dist(A:Point, B:Point, C:Point, D:Point) Test for equal distance d(AB) = d(CD).
fixedpoint(A:Point, B:Point, u:Scalar) The point $D=(1-u)*A+u*B$ on the line AB for a fixed value of u.
intersection_point(a:Line, b:Line) The intersection point of the lines $a,b$ .
is_cc_tangent(c1:Circle, c2:Circle) Zero iff circles $c_1$ and $c_2$ are tangent.
is_cl_tangent(c:Circle, l:Line) Zero iff the line $l$ is tangent to the circle $c$ .
is_collinear(A:Point, B:Point, C:Point) Zero iff $A,B,C$ are on a common line. For the signed area of the triangle $ABC$ use triangle_area.
is_concurrent(a:Line, b:Line, c:Line) Zero iff the lines $a,b,c$ pass through a common point.
is_concyclic(A:Point, B:Point, C:Point, D:Point) Zero iff four given points are on a common circle.
is_equal(A:Scalar, B:Scalar) Test for equality of A and B.
is_orthogonal(a:Line, b:Line) zero iff the lines $a,b$ are orthogonal.
is_parallel(a:Line, b:Line) Zero iff the lines $a,b$ are parallel.
l2_angle(a:Line, b:Line) Tangens of the angle between $a$ and $b$ .
line_slider(a:Line, u:Scalar) Chooses a point on $a$ using parameter $u$ .
median(A:Point, B:Point, C:Point) The median line from $A$ to $BC$ .
midpoint(A:Point, B:Point) The midpoint of $AB$ .
on_bisector(P:Point, A:Point, B:Point, C:Point) Zero iff $P$ is a point on the (inner or outer) bisector of the angle $\angle ABC$ .
on_circle(P:Point, c:Circle) Zero iff $P$ is on the circle $c$ .
on_line(P:Point, a:Line) Zero iff $P$ is on the line $a$ .
ortho_line(P:Point, a:Line) The line through $P$ orthogonal to the line $a$ .
orthocenter(A:Point, B:Point, C:Point) Orthocenter of the triangle $ABC$ .
other_cc_point(P:Point, c1:Circle, c2:Circle) $c_1$ and $c_2$ intersect at $P$ . The procedure returns the second intersection point.
other_cl_point(P:Point, c:Circle, l:Line) $c$ and $l$ intersect at $P$ . The procedure returns the second intersection point.
other_incenter(M:Point, A:Point, B:Point) Let $ABC$ be a triangle and $M$ the incenter of $ABC$ . Returns the excenter of $ABC$ on the bisector $CM$ .
p3_angle(A:Point, B:Point, C:Point) Tangens of the angle between $BA$ and $BC$ .
p3_circle(A:Point, B:Point, C:Point) The circle through 3 given points.
p9_center(A:Point, B:Point, C:Point) Center of the nine-point circle of the triangle $ABC$ .
p9_circle(A:Point, B:Point, C:Point) The nine-point circle (Feuerbach circle) of the triangle $ABC$ .
p_bisector(B:Point, C:Point) The perpendicular bisector of $BC$ .
pappus_line(A:Point, B:Point, C:Point, D:Point, E:Point, F:Point) The Pappus line of a conic 6-tuple of points.
par_line(P:Point, a:Line) The line through $P$ parallel to line $a$ .
par_point(A:Point, B:Point, C:Point) Point D that makes $ABCD$ a parallelogram.
pc_circle(M:Point, A:Point) The circle with given center $M$ and circumfere point $A$ .
pedalpoint(P:Point, a:Line) The pedal point of the perpendicular from $P$ onto $a$ .
pp_line(A:Point, B:Point) The line through $A$ and $B$ .
radical_axis(c1:Circle, c2:Circle) The radical axis of two circles, i.e. the line of point with equal pc_degree wrt. to both circles. If the circles intersect this is the line through their intersection points. If the circles don't intersect this are the point with equal tangent segments to both circles.
rotate(C:Point, A:Point, angle:Scalar) Rotate point A (counterclockwise) around center C with angle angle*Pi.
sqrdist(A:Point, B:Point) Squared distance between $A$ and $B$ .
sqrdist_pl(A:Point, l:Line) Squared distance between point $A$ and line $l$ .
sym_line(a:Line, l:Line) The line symmetric to $a$ wrt. the line $l$ .
sym_point(P:Point, l:Line) The point symmetric to $P$ wrt. line $l$ .
triangle_area(A:Point, B:Point, C:Point) Signed area of the directed triangle $ABC$ .
varpoint(A:Point, B:Point, u:Scalar) The point $D=(1-u)*A+u*B$ that slides on the line AB, with parameter u.

Acknowledgements

Malte Witte translated the code of version 1.1 from Reduce to Maple, MuPAD, and Mathematica and compiled many examples for the SymbolicData GEO proof scheme collection, mainly from Chou's book.

Benjamin Friedrich collected examples and solutions with geometric background from IMO contests.

AUTHOR	:	Hans-Gert Graebe
ADDRESS	:	Univ. Leipzig, Institut f. Informatik, D - 04109 Leipzig, Germany
URL	:	http://www.informatik.uni-leipzig.de/~graebe

Point(a:Scalar, b:Scalar)	Point constructor. Returns a coding for the point with coordinates (a,b).
altitude(A:Point, B:Point, C:Point)	The altitude from $A$ onto $g(BC)$ .
angle_sum(a:Scalar, b:Scalar)	Returns $tan(alpha+beta)$ , if $a=tan(alpha), b=tan(beta)$ .
centroid(A:Point, B:Point, C:Point)	Centroid of the triangle $ABC$ .
circle_center(c:Circle)	The center of the circle $c$ .
circle_slider(M:Point, A:Point, u:Scalar)	Choose a point on the circle with center $M$ and point $A$ on the perimeter using a rational parametrization with parameter $u$ .
circle_sqradius(c:Circle)	The squared radius of the circle $c$ .
circumcenter(A:Point, B:Point, C:Point)	The circumcenter of the triangle $ABC$ .
csym_point(P:Point, Q:Point)	The point symmetric to $P$ wrt. $Q$ as symmetry center.
eq_angle(A:Point, B:Point, C:Point, D:Point, E:Point, F:Point)	Test for equal angle w(ABC) = w(DEF).
eq_dist(A:Point, B:Point, C:Point, D:Point)	Test for equal distance d(AB) = d(CD).
fixedpoint(A:Point, B:Point, u:Scalar)	The point $D=(1-u)A+uB$ on the line AB for a fixed value of u.
intersection_point(a:Line, b:Line)	The intersection point of the lines $a,b$ .
is_cc_tangent(c1:Circle, c2:Circle)	Zero iff circles $c_1$ and $c_2$ are tangent.
is_cl_tangent(c:Circle, l:Line)	Zero iff the line $l$ is tangent to the circle $c$ .
is_collinear(A:Point, B:Point, C:Point)	Zero iff $A,B,C$ are on a common line. For the signed area of the triangle $ABC$ use `triangle_area`.
is_concurrent(a:Line, b:Line, c:Line)	Zero iff the lines $a,b,c$ pass through a common point.
is_concyclic(A:Point, B:Point, C:Point, D:Point)	Zero iff four given points are on a common circle.
is_equal(A:Scalar, B:Scalar)	Test for equality of A and B.
is_orthogonal(a:Line, b:Line)	zero iff the lines $a,b$ are orthogonal.
is_parallel(a:Line, b:Line)	Zero iff the lines $a,b$ are parallel.
l2_angle(a:Line, b:Line)	Tangens of the angle between $a$ and $b$ .
line_slider(a:Line, u:Scalar)	Chooses a point on $a$ using parameter $u$ .
median(A:Point, B:Point, C:Point)	The median line from $A$ to $BC$ .
midpoint(A:Point, B:Point)	The midpoint of $AB$ .
on_bisector(P:Point, A:Point, B:Point, C:Point)	Zero iff $P$ is a point on the (inner or outer) bisector of the angle $\angle ABC$ .
on_circle(P:Point, c:Circle)	Zero iff $P$ is on the circle $c$ .
on_line(P:Point, a:Line)	Zero iff $P$ is on the line $a$ .
ortho_line(P:Point, a:Line)	The line through $P$ orthogonal to the line $a$ .
orthocenter(A:Point, B:Point, C:Point)	Orthocenter of the triangle $ABC$ .
other_cc_point(P:Point, c1:Circle, c2:Circle)	$c_1$ and $c_2$ intersect at $P$ . The procedure returns the second intersection point.
other_cl_point(P:Point, c:Circle, l:Line)	$c$ and $l$ intersect at $P$ . The procedure returns the second intersection point.
other_incenter(M:Point, A:Point, B:Point)	Let $ABC$ be a triangle and $M$ the incenter of $ABC$ . Returns the excenter of $ABC$ on the bisector $CM$ .
p3_angle(A:Point, B:Point, C:Point)	Tangens of the angle between $BA$ and $BC$ .
p3_circle(A:Point, B:Point, C:Point)	The circle through 3 given points.
p9_center(A:Point, B:Point, C:Point)	Center of the nine-point circle of the triangle $ABC$ .
p9_circle(A:Point, B:Point, C:Point)	The nine-point circle (Feuerbach circle) of the triangle $ABC$ .
p_bisector(B:Point, C:Point)	The perpendicular bisector of $BC$ .
pappus_line(A:Point, B:Point, C:Point, D:Point, E:Point, F:Point)	The Pappus line of a conic 6-tuple of points.
par_line(P:Point, a:Line)	The line through $P$ parallel to line $a$ .
par_point(A:Point, B:Point, C:Point)	Point D that makes $ABCD$ a parallelogram.
pc_circle(M:Point, A:Point)	The circle with given center $M$ and circumfere point $A$ .
pedalpoint(P:Point, a:Line)	The pedal point of the perpendicular from $P$ onto $a$ .
pp_line(A:Point, B:Point)	The line through $A$ and $B$ .
radical_axis(c1:Circle, c2:Circle)	The radical axis of two circles, i.e. the line of point with equal pc_degree wrt. to both circles. If the circles intersect this is the line through their intersection points. If the circles don't intersect this are the point with equal tangent segments to both circles.
rotate(C:Point, A:Point, angle:Scalar)	Rotate point A (counterclockwise) around center C with angle angle*Pi.
sqrdist(A:Point, B:Point)	Squared distance between $A$ and $B$ .
sqrdist_pl(A:Point, l:Line)	Squared distance between point $A$ and line $l$ .
sym_line(a:Line, l:Line)	The line symmetric to $a$ wrt. the line $l$ .
sym_point(P:Point, l:Line)	The point symmetric to $P$ wrt. line $l$ .
triangle_area(A:Point, B:Point, C:Point)	Signed area of the directed triangle $ABC$ .
varpoint(A:Point, B:Point, u:Scalar)	The point $D=(1-u)A+uB$ that slides on the line AB, with parameter u.