Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries (Q2631966)

Written for ``practitioners of symbolic computation or automated theorem proving,'' this is a survey of undecidability results for elementary (first-order) geometries, with particular emphasis on ``affine incidence geometry, Hilbert-style Euclidean geometry, Wu's orthogonal geometry and Origami geometry.'' The author shows \(\bullet\) how the segment calculus allows for a transfer of the undecidability results known to hold for theories of fields to that of elementary geometries, \(\bullet\) how the result by \textit{M. Ziegler} [Enseign. Math., II. Sér. 28, 269--280 (1982; Zbl 0519.12018)], which states that every finitely axiomatized field theory that has \(\mathbb{R}\) or \(\mathbb{C}\) as a model is hereditarily undecidable, can be used to prove the undecidability of a plethora of finitely axiomatized elementary geometries, and \(\bullet\) that the consequences in the universal fragment of geometries over fields are decidable. He also indicates that these results can be extended to projective, elliptic, hyperbolic, and higher-dimensional geometries.