Rewriting input expressions in complex algebraic geometry provers

DOI10.1007/S10472-018-9590-1MaRDI QIDQ2631957zbMATH OpenOpenAlexFDO

Authors Zoltán Kovács, C. Sólyom-Gecse, Tomas Recio

Publication date 16 May 2019

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

Full work available at URL https://doi.org/10.1007/s10472-018-9590-1

zbMATH Keywords

automatic theorem deductionautomatic theorem provingcomplex algebraic geometrydynamic geometry softwareelementary geometry

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to commutative algebra (13-04) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10) Effectivity, complexity and computational aspects of algebraic geometry (14Q20) Software, source code, etc. for problems pertaining to geometry (51-04)

Review text

The use of dynamic geometry by complex algebraic provers help to understand both the input and the output of classical theorems that involve Euclidean geometry. For dynamic geometry to exist, there must be an algebraic formulation behind. This may seem simple, but it is highly complex. The programmer has to consider degenerate situations and different situations over the complex numbers when formulating correctly. This work offers illustrative examples of this problem and its authors are experts in this field. By using classical tools of commutative algebra, such as elimination ideals and Groebner basis, in Section 4 the authors present an algorithm to convert expressions having non-negative quantities (like distances) in Euclidean geometry theorems to be usable in a complex algebraic geometry prover.

Recommendations

• On the algebraic formulation of certain geometry statements and mechanical geometry theorem proving
• scientific article; zbMATH DE number 1303337
• scientific article; zbMATH DE number 1222429
• Proving geometry theorems with rewrite rules
• A new approach for automatic theorem proving in real geometry

Cites work

• A new approach for automatic theorem proving in real geometry
• An introduction to Java geometry expert. (Extended abstract)
• Automated theorem proving in GeoGebra: current achievements
• Automatic discovery of theorems in elementary geometry
• Computational Science and Its Applications – ICCSA 2004
• Development of automatic reasoning tools in GeoGebra
• scientific article; zbMATH DE number 41286 (Why is no real title available?)
• scientific article; zbMATH DE number 3586510 (Why is no real title available?)
• Ideals, varieties, and algorithms. An introduction to computational algebraic geometry and commutative algebra
• Using Gröbner bases to reason about geometry problems

Cited in

(4)

• Two almost-circles, and two real ones
• scientific article; zbMATH DE number 67429 (Why is no real title available?)
• Open geometry prover community project
• Supporting proving and discovering geometric inequalities in GeoGebra by using Tarski

Describes a project that uses

Uses Software

• SINGULAR
• GeoGebra
• OpenGeoProver
• JGEX
• GEX

This page was built for publication: Rewriting input expressions in complex algebraic geometry provers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2631957)