Solving Some Geometry Problems of the Náboj 2023 Contest with Automated Deduction in GeoGebra Discovery
This work addresses geometry contest problems for educators and automated reasoning researchers, but it is incremental as it applies an existing tool to new problems.
The paper tackled geometry problems from the Náboj 2023 contest by using GeoGebra Discovery for automated deduction, requiring symbolic computations, and analyzed the difficulty of inputting problems to improve future tractability.
In this article, we solve some of the geometry problems of the Náboj 2023 competition with the help of a computer, using examples that the software tool GeoGebra Discovery can calculate. In each case, the calculation requires symbolic computations. We analyze the difficulty of feeding the problem into the machine and set further goals to make the problems of this type of contests even more tractable in the future.