On protocols for the automated discovery of theorems in elementary geometry

DOI10.1007/s10817-009-9133-xzbMath1184.68458OpenAlexW1983376640MaRDI QIDQ846167

Tomás Recio, Giorgio Dalzotto

Publication date: 1 February 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9133-x

zbMATH Keywords

computational algebraic geometryautomatic theorem provingelementary geometryautomatic theorem discovery

Mathematics Subject Classification ID

Software, source code, etc. for problems pertaining to geometry (51-04) Computational aspects in algebraic geometry (14Q99)

Related Items

On the unavoidable uncertainty of truth in dynamic geometry proving ⋮ Detecting truth, just on parts ⋮ Automated reducible geometric theorem proving and discovery by Gröbner basis method ⋮ Some issues on the automatic computation of plane envelopes in interactive environments ⋮ Generalizing the Steiner-Lehmus theorem using the Gröbner cover ⋮ Automatic Discovery of Geometry Theorems Using Minimal Canonical Comprehensive Gröbner Systems ⋮ Towards the Automatic Discovery of Theorems in GeoGebra ⋮ On One Method of Proving Inequalities in Automated Way ⋮ A mechanical geometer ⋮ Dealing with negative conditions in automated proving: tools and challenges. The unexpected consequences of Rabinowitsch's trick ⋮ Development of automatic reasoning tools in GeoGebra ⋮ Automated generation of geometric theorems from images of diagrams

Uses Software

• CoCoA
• Epsilon

Cites Work

• A new theorem discovered by computer prover
• A method for the mechanical derivation of formulas in elementary geometry
• Wu's method and its application to perspective viewing
• Automatic discovery of theorems in elementary geometry
• Computational Science and Its Applications – ICCSA 2004
• Automatic Discovery of Geometry Theorems Using Minimal Canonical Comprehensive Gröbner Systems
• Automated Deduction in Geometry
• Automated Deduction in Geometry
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item