Modular algebraic specification of some basic geometrical constructions (Q1115574)

Application of the algebraic specification method to plane geometry is investigated. The basic constructions such as the line through two points, the intersection of two lines, the circle through three points, and the tangent to a circle through a point are specified in a variant of the OBJ language. The real numbers are required in geometry. However the reals are an uncountable structure, which therefore cannot be specified with initial algebra semantics. Luckily all the geometric constructions given in the paper only need square roots of nonnegative elements and thus may be specified in a conventional way. The paper indicates how a rigorous semantic foundation in equational logic can be given for many techniques in knowledge representation.