plangeo1 http://www.win.tue.nl/~amc/oz/om/cds/plangeo1.ocd 2006-06-01 experimental 2004-06-01 0 5 This CD defines symbols for planar Euclidean geometry. point The symbol is used to indicate a point of planar Euclidean geometry by a variable. The point may (but need not) be subject to constraints. The symbol takes the variable as the first argument and the constraints as further arguments. Given two lines l and m, a point A on l and m is defined by: line The symbol is used to indicate a line of planar Euclidean geometry by a variable. The line may (but need not) be subject to constraints. The symbol takes the variable as the first argument and the constraints as further arguments. Given points A and B, a line l through A and B is defined by: incident The symbol represents the logical incidence function which is a binary function taking arguments representing geometric objects like points and lines and returning a boolean value. It is true if and only if the first argument is incident to the second. That a point A is incident to a line l is given by: configuration The symbol represents a configuration in Euclidean planar geometry consisting of a sequence of geometric objects like points, lines, etc, but also of other configurations. The configuration of a point A and a line l incident to A is defined by: The prevous configuration of a point A and a line l incident with A can be extended by adding a second point B incident with l: We describe a triangle on the distinct points A, B, C and lines a, b, c: type The symbol represents the type of the basic geometric objects: points, lines, configuration. If A and B are objects of the same type, then they are not incident. assertion The symbol is a constructor with two arguments. Its first argument should be a configuration, its second argument a statement about the configuration, called thesis. When applied to a configuration C and a thesis T, the OpenMath object assertion(C,T) expresses the assertion that T holds in C. The assertion that two distinct lines meet in only one point can be expressed as follows using the assertion symbol. are_on_line The statement that a set of points is collinear. This example states that A, B, C, and D are collinear.