GeoGebra Tools with Proof Capabilities
We report about significant enhancements of the complex algebraic geometry theorem proving subsystem in GeoGebra for automated proofs in Euclidean geometry, concerning the extension of numerous GeoGebra tools with proof capabilities. As a result, a number of elementary theorems can be proven by using GeoGebra's intuitive user interface on various computer architectures including native Java and web based systems with JavaScript. We also provide a test suite for benchmarking our results with 200 test cases.
Code (0)
등록된 구현이 없습니다.
Tasks
Automated Theorem ProvingBenchmarkingSimilar Papers 제목 키워드 기반
Showing Proofs, Assessing Difficulty with GeoGebra Discovery
In our contribution we describe some on-going improvements concerning the Automated Reasoning Tools developed in GeoGebra Discovery, providing different examples of the performance of these new features. We describe the …
Solving with GeoGebra Discovery an Austrian Mathematics Olympiad problem: Lessons Learned
We address, through the automated reasoning tools in GeoGebra Discovery, a problem from a regional phase of the Austrian Mathematics Olympiad 2023. Trying to solve this problem gives rise to four different kind of feedba…
Towards Automated Discovery of Geometrical Theorems in GeoGebra
We describe a prototype of a new experimental GeoGebra command and tool Discover that analyzes geometric figures for salient patterns, properties, and theorems. This tool is a basic implementation of automated discovery …
Solving Some Geometry Problems of the Náboj 2023 Contest with Automated Deduction in GeoGebra Discovery
In this article, we solve some of the geometry problems of the N\'aboj 2023 competition with the help of a computer, using examples that the software tool GeoGebra Discovery can calculate. In each case, the calculation r…
Newclid: A User-Friendly Replacement for AlphaGeometry
We introduce a new symbolic solver for geometry, called Newclid, which is based on AlphaGeometry. Newclid contains a symbolic solver called DDARN (derived from DDAR-Newclid), which is a significant refactoring and upgrad…