geoprover.html 9.9 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154
  1. <html>
  2. <head>
  3. <title>GeoProver v. 1.3a</title>
  4. </head>
  5. <body>
  6. <h1 align="center">The GeoProver Package for Mechanized (Plane) Geometry Theorem Proving
  7. <p> Version 1.3a</h1>
  8. <h3 align="center">
  9. <table>
  10. <tr><td>AUTHOR <td>: <td>Hans-Gert Graebe
  11. <tr><td> ADDRESS <td>: <td>Univ. Leipzig, Institut f. Informatik, D - 04109 Leipzig, Germany
  12. <tr><td> URL <td>:
  13. <td> <a href="http://www.informatik.uni-leipzig.de/~graebe">http://www.informatik.uni-leipzig.de/~graebe</a>
  14. </table>
  15. </h3>
  16. <h4>Introduction</h4>
  17. <p>The <b>GeoProver</b> is a small package for
  18. mechanized (plane) geometry manipulations with non degeneracy
  19. tracing, available for different CAS platforms (Maple, MuPAD,
  20. Mathematica, and Reduce).</p>
  21. <p>It provides the casual user with a couple of procedures that
  22. allow him/her to mechanize his/her own geometry proofs. Version
  23. 1.1 grew out from a course of lectures for students of computer
  24. science on this topic held by the author at the Univ. of Leipzig
  25. in fall 1996 and was updated after a similar lecture in spring
  26. 1998. </p>
  27. <p>The (completely revised) version 1.2, finished in March 2002,
  28. was set up as a generic software project to manage the code for
  29. different platforms in a unified way. There is a close relationship
  30. to the SymbolicData project (see
  31. <url>http://www.symbolicdata.org</url>).
  32. <p>For examples we refer to the test file, but also to the
  33. SymbolicData GEO collection. It contains many (generic) proof
  34. schemes of geometry theorems, mainly from Chou's book. These proof
  35. schemes can be translated to the GeoProver syntax for different
  36. platforms with SymbolicData tools.</p>
  37. <p>For version 1.3 the syntax definition (the <b>GeoCode</b>) was
  38. separated from the GeoProver implementation. The latter is an
  39. implementation of the GeoCode standard using the coordinate
  40. method. </p>
  41. <p>Note that function names change with different versions of the
  42. GeoCode standard. GeoProver 1.3 implements the GeoCode standard
  43. 1.3. </p>
  44. <p>Please send comments, bug reports, hints, wishes, criticisms
  45. etc. to the author.</p>
  46. <h4>Basic Data Types</h4>
  47. <p>Basic data types are <b>Points</b>, <b>Lines</b>, and
  48. <b>Circles</b>.</p>
  49. <p>A point <code>A:=Point(a,b)</code> represents a point with
  50. coordinates <math>(a1,a2)</math>. </p>
  51. <p>A line <code>l:=Line(a,b,c)</code> represents the line
  52. <math>{ (x,y) : a*x+b*y+c=0 }</math>. </p>
  53. <p>A circle <code>c:=Circle(c1,c2,c3,c4)</code> represents the
  54. circle <math>{ (x,y) : c1*(x^2+y^2)+c2*x+c3*y+c4=0 }</math>. </p>
  55. <h4>Available functions</h4>
  56. <p><table border align="center" cellpadding=8 width="80%">
  57. <tr><td align="center"> Point(a:Scalar, b:Scalar) <td> Point constructor. Returns a coding for the point with
  58. coordinates (a,b).
  59. <tr><td align="center"> altitude(A:Point, B:Point, C:Point) <td> The altitude from <math>A</math> onto <math>g(BC)</math>.
  60. <tr><td align="center"> angle_sum(a:Scalar, b:Scalar) <td> Returns <math>tan(alpha+beta)</math>, if <math>a=tan(alpha), b=tan(beta)</math>.
  61. <tr><td align="center"> centroid(A:Point, B:Point, C:Point) <td> Centroid of the triangle <math>ABC</math>.
  62. <tr><td align="center"> circle_center(c:Circle) <td> The center of the circle <math>c</math>.
  63. <tr><td align="center"> circle_slider(M:Point, A:Point, u:Scalar) <td> Choose a point on the circle with center <math>M</math> and point
  64. <math>A</math> on the perimeter using a rational parametrization with
  65. parameter <math>u</math>.
  66. <tr><td align="center"> circle_sqradius(c:Circle) <td> The squared radius of the circle <math>c</math>.
  67. <tr><td align="center"> circumcenter(A:Point, B:Point, C:Point) <td> The circumcenter of the triangle <math>ABC</math>.
  68. <tr><td align="center"> csym_point(P:Point, Q:Point) <td> The point symmetric to <math>P</math> wrt. <math>Q</math> as symmetry center.
  69. <tr><td align="center"> eq_angle(A:Point, B:Point, C:Point, D:Point, E:Point, F:Point) <td> Test for equal angle w(ABC) = w(DEF).
  70. <tr><td align="center"> eq_dist(A:Point, B:Point, C:Point, D:Point) <td> Test for equal distance d(AB) = d(CD).
  71. <tr><td align="center"> fixedpoint(A:Point, B:Point, u:Scalar) <td> The point <math>D=(1-u)*A+u*B</math> on the line AB for a fixed value of u.
  72. <tr><td align="center"> intersection_point(a:Line, b:Line) <td> The intersection point of the lines <math>a,b</math>.
  73. <tr><td align="center"> is_cc_tangent(c1:Circle, c2:Circle) <td> Zero iff circles <math>c_1</math> and <math>c_2</math> are tangent.
  74. <tr><td align="center"> is_cl_tangent(c:Circle, l:Line) <td> Zero iff the line <math>l</math> is tangent to the circle <math>c</math>.
  75. <tr><td align="center"> is_collinear(A:Point, B:Point, C:Point) <td> Zero iff <math>A,B,C</math> are on a common line. For the signed area
  76. of the triangle <math>ABC</math> use <tt>triangle_area</tt>.
  77. <tr><td align="center"> is_concurrent(a:Line, b:Line, c:Line) <td> Zero iff the lines <math>a,b,c</math> pass through a common point.
  78. <tr><td align="center"> is_concyclic(A:Point, B:Point, C:Point, D:Point) <td> Zero iff four given points are on a common circle.
  79. <tr><td align="center"> is_equal(A:Scalar, B:Scalar) <td> Test for equality of A and B.
  80. <tr><td align="center"> is_orthogonal(a:Line, b:Line) <td> zero iff the lines <math>a,b</math> are orthogonal.
  81. <tr><td align="center"> is_parallel(a:Line, b:Line) <td> Zero iff the lines <math>a,b</math> are parallel.
  82. <tr><td align="center"> l2_angle(a:Line, b:Line) <td> Tangens of the angle between <math>a</math> and <math>b</math>.
  83. <tr><td align="center"> line_slider(a:Line, u:Scalar) <td> Chooses a point on <math>a</math> using parameter <math>u</math>.
  84. <tr><td align="center"> median(A:Point, B:Point, C:Point) <td> The median line from <math>A</math> to <math>BC</math>.
  85. <tr><td align="center"> midpoint(A:Point, B:Point) <td> The midpoint of <math>AB</math>.
  86. <tr><td align="center"> on_bisector(P:Point, A:Point, B:Point, C:Point) <td> Zero iff <math>P</math> is a point on the (inner or outer) bisector of the
  87. angle <math>\angle ABC</math>.
  88. <tr><td align="center"> on_circle(P:Point, c:Circle) <td> Zero iff <math>P</math> is on the circle <math>c</math>.
  89. <tr><td align="center"> on_line(P:Point, a:Line) <td> Zero iff <math>P</math> is on the line
  90. <math>a</math>.
  91. <tr><td align="center"> ortho_line(P:Point, a:Line) <td> The line through <math>P</math> orthogonal to the line <math>a</math>.
  92. <tr><td align="center"> orthocenter(A:Point, B:Point, C:Point) <td> Orthocenter of the triangle <math>ABC</math>.
  93. <tr><td align="center"> other_cc_point(P:Point, c1:Circle, c2:Circle) <td> <math>c_1</math> and <math>c_2</math> intersect at <math>P</math>.
  94. The procedure returns the second intersection point.
  95. <tr><td align="center"> other_cl_point(P:Point, c:Circle, l:Line) <td> <math>c</math> and <math>l</math> intersect at <math>P</math>.
  96. The procedure returns the second intersection point.
  97. <tr><td align="center"> other_incenter(M:Point, A:Point, B:Point) <td> Let <math>ABC</math> be a triangle and <math>M</math> the incenter of
  98. <math>ABC</math>. Returns the excenter of <math>ABC</math> on the bisector
  99. <math>CM</math>.
  100. <tr><td align="center"> p3_angle(A:Point, B:Point, C:Point) <td> Tangens of the angle between <math>BA</math> and <math>BC</math>.
  101. <tr><td align="center"> p3_circle(A:Point, B:Point, C:Point) <td> The circle through 3 given points.
  102. <tr><td align="center"> p9_center(A:Point, B:Point, C:Point) <td> Center of the nine-point circle of the triangle <math>ABC</math>.
  103. <tr><td align="center"> p9_circle(A:Point, B:Point, C:Point) <td> The nine-point circle (Feuerbach circle) of the triangle <math>ABC</math>.
  104. <tr><td align="center"> p_bisector(B:Point, C:Point) <td> The perpendicular bisector of <math>BC</math>.
  105. <tr><td align="center"> pappus_line(A:Point, B:Point, C:Point, D:Point, E:Point, F:Point) <td> The Pappus line of a conic 6-tuple of points.
  106. <tr><td align="center"> par_line(P:Point, a:Line) <td> The line through <math>P</math> parallel to line <math>a</math>.
  107. <tr><td align="center"> par_point(A:Point, B:Point, C:Point) <td> Point D that makes <math>ABCD</math> a parallelogram.
  108. <tr><td align="center"> pc_circle(M:Point, A:Point) <td> The circle with given center <math>M</math> and circumfere point <math>A</math>.
  109. <tr><td align="center"> pedalpoint(P:Point, a:Line) <td> The pedal point of the perpendicular from <math>P</math> onto <math>a</math>.
  110. <tr><td align="center"> pp_line(A:Point, B:Point) <td> The line through <math>A</math> and <math>B</math>.
  111. <tr><td align="center"> radical_axis(c1:Circle, c2:Circle) <td> The radical axis of two circles, i.e. the line of point with equal pc_degree
  112. wrt. to both circles. If the circles intersect this is the line through their
  113. intersection points. If the circles don't intersect this are the point with
  114. equal tangent segments to both circles.
  115. <tr><td align="center"> rotate(C:Point, A:Point, angle:Scalar) <td> Rotate point A (counterclockwise) around center C with angle angle*Pi.
  116. <tr><td align="center"> sqrdist(A:Point, B:Point) <td> Squared distance between <math>A</math> and <math>B</math>.
  117. <tr><td align="center"> sqrdist_pl(A:Point, l:Line) <td> Squared distance between point <math>A</math> and line
  118. <math>l</math>.
  119. <tr><td align="center"> sym_line(a:Line, l:Line) <td> The line symmetric to <math>a</math> wrt. the line <math>l</math>.
  120. <tr><td align="center"> sym_point(P:Point, l:Line) <td> The point symmetric to <math>P</math> wrt. line <math>l</math>.
  121. <tr><td align="center"> triangle_area(A:Point, B:Point, C:Point) <td> Signed area of the directed triangle <math>ABC</math>.
  122. <tr><td align="center"> varpoint(A:Point, B:Point, u:Scalar) <td> The point <math>D=(1-u)*A+u*B</math> that slides on the line
  123. AB, with parameter u.
  124. </table>
  125. <h4>Acknowledgements</h4>
  126. <p>Malte Witte translated the code of version 1.1 from Reduce to
  127. Maple, MuPAD, and Mathematica and compiled many examples for the
  128. SymbolicData GEO proof scheme collection, mainly from Chou's
  129. book.</p>
  130. <p>Benjamin Friedrich collected examples and solutions with
  131. geometric background from IMO contests.</p>
  132. </body>
  133. </html>