plangeo1 http://www.win.tue.nl/~amc/oz/om/cds/plangeo1.ocd 00 unofficial 2002-03-15 0.1 0 logic1.ocd relation1.ocd 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.