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

DOI10.1007/S10472-018-9610-1zbMath1439.03033arXiv1712.07474OpenAlexW2778452107WikidataQ128785024 ScholiaQ128785024MaRDI QIDQ2631966

Johann A. Makowsky

Publication date: 16 May 2019

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1712.07474

zbMATH Keywords

undecidabilityEuclidean geometryautomated theorem proving

Mathematics Subject Classification ID

Undecidability and degrees of sets of sentences (03D35) Decidability of theories and sets of sentences (03B25) Euclidean geometries (general) and generalizations (51M05)

Related Items (2)

Axiomatizing origami planes ⋮ STRONGLY MINIMAL STEINER SYSTEMS I: EXISTENCE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On a question of Abraham Robinson
• Algorithmic uses of the Feferman-Vaught theorem
• Some new results on decidability for elementary algebra and geometry
• Elimination of quantifiers in algebraic structures
• Basic principles of mechanical theorem proving in elementary geometries
• Real quantifier elimination is doubly exponential
• A refutational approach to geometry theorem proving
• Mechanical theorem proving in geometries. Basic principles. Transl. from the Chinese by Xiaofan Jin and Dongming Wang
• A mathematical theory of origami constructions and numbers
• Formalization of the arithmetization of Euclidean plane geometry and applications
• From geometry to conceptual relativity
• Definability and decidability in infinite algebraic extensions
• Orthogonality as single primitive notion for metric planes
• Axiomatizing geometric constructions
• Undecidable theories
• Proof and Computation in Geometry
• Über Metatheoretische Eigenschaften Einiger Geometrischer Theorien
• Rekursive Unentscheidbarkeit der Theorie der pythagoräischen Körper
• Tarski's System of Geometry
• Ternary Operations as Primitive Notions for Constructive Plane Geometry V
• COMPLEXITY AND REAL COMPUTATION: A MANIFESTO
• Model Theory and the Philosophy of Mathematical Practice
• Axiomatizing Changing Conceptions of the Geometric Continuum I: Euclid-Hilbert†
• Unentscheidbarkeit Der Euklidischen Inzidenzgeometrie
• MORITA EQUIVALENCE
• Definability and decision problems in arithmetic
• Projective Planes
• A FORMAL SYSTEM FOR EUCLID’SELEMENTS
• Logical Approaches to Computational Barriers
• Algorithms in real algebraic geometry
• Defining \(\mathbb Z\) in \(\mathbb Q\)

This page was built for publication: Can one design a geometry engine? Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries