plangeo3 http://www.openmath.org/cd http://www.openmath.org/cd/plangeo3.ocd 2006-06-01 experimental 2004-06-01 0 3 This CD defines symbols for planar Euclidean geometry related to distance. distance The distance between two affine points is the Euclidean distance. The distance between two geometric objects O and O' is the infimum of the distances between two affine points, one on O and one on O'. The distance between two points A and B. perpendicular perpendicular is a binary boolean function with input two lines, halflines or segments. Its value is true whenever the two inputs are perpendicular to each other. Testing perpendicularity of two lines L and M. parallel parallel is a binary boolean function with input two lines, halflines or segments. Its value is true whenever the two inputs are parallel. Testing parallelism of two lines L and M. circle The symbol represents a circle. The circle may be subject to constraints. The circle C with center A and radius 1 is given by 1 radius The radius of a circle. The assertion that the radius of the circle C is 1: 1 radius_of Gives the radius of a circle. The radius of the circle C is given by center Defines the center of a circle. The circle C with center A and radius 1 is given by 1 center_of Gives the center of the circle If C is the circle of the previous example then the following gives A. are_on_circle The statement that a set of points is on one circle. This example states that A, B, C, and D lie on one circle. angle Angle of a corner, always measured in positive (anti-clockwise) direction. Notice that are not the same. midpoint The midpoint between two points or two endpoints of a segment. The midpoint of two points A and B is the same as the midpoint of the segment S on A and B. equals is_midpoint The statement that one point is the midpoint of two others. This example states that C is the midpoint of A and B. center_of_gravity Center of gravity of a number of points. The center of gravity G of three points A, B and C is defined as follows. perpbisector Given two distinct points A and B, this is the line of all points at equal distance to both A and B. altitude Given a point p and a line L, this defines the segment starting at p and ending in the unique point of L closest to p. perpline Given a point p and a line L, this defines the line through p perpendicular to L. polarline Given a point p and a circle C this defines the polar line of p with respect to C. If p is incident with the circle C, the polar line of p with respect to C is the tangent line at p with respect to C. tangent Given a line L and a circle C this boolean checks whether L is a tangent line to C. arc an arc of a circle M from A to B is the set of points of M that are encountered when traversing the circle clockwise from A to B.