Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Showing Proofs, Assessing Difficulty with GeoGebra Discovery

Zoltán Kovács, Tomás Recio, M. Pilar Vélez

TL;DR

The paper addresses the challenge of making automated geometric proofs in GeoGebra Discovery transparent by introducing ShowProof, which visualizes the algebraic reasoning steps and certificates, and by proposing a syzygy-based difficulty metric for geometric statements. It formalizes a complexity measure where the difficulty of a statement H ⇒ T is tied to the maximum degree of the syzygies expressing T (or $1$) as a combination of the hypotheses, and it employs the Rabinowitsch trick to certify ideal membership. Through three illustrative examples, the authors demonstrate how the certificate and its degree depend on equation representations and numerical specialization, revealing that the same geometric claim can exhibit different measured complexities. The work lays groundwork for evaluating and comparing automated geometric proofs and suggests further exploration into more complex problems and the theoretical relationship between expression complexity and decidability in this algebraic geometric framework.

Abstract

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 new ShowProof command, that outputs both the sequence of the different steps performed by GeoGebra Discovery to confirm a certain statement, as well as a number intending to grade the difficulty or interest of the assertion. The proposal of this assessment measure, involving the comparison of the expression of the thesis (or conclusion) as a combination of the hypotheses, will be developed.

Showing Proofs, Assessing Difficulty with GeoGebra Discovery

TL;DR

The paper addresses the challenge of making automated geometric proofs in GeoGebra Discovery transparent by introducing ShowProof, which visualizes the algebraic reasoning steps and certificates, and by proposing a syzygy-based difficulty metric for geometric statements. It formalizes a complexity measure where the difficulty of a statement H ⇒ T is tied to the maximum degree of the syzygies expressing T (or ) as a combination of the hypotheses, and it employs the Rabinowitsch trick to certify ideal membership. Through three illustrative examples, the authors demonstrate how the certificate and its degree depend on equation representations and numerical specialization, revealing that the same geometric claim can exhibit different measured complexities. The work lays groundwork for evaluating and comparing automated geometric proofs and suggests further exploration into more complex problems and the theoretical relationship between expression complexity and decidability in this algebraic geometric framework.

Abstract

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 new ShowProof command, that outputs both the sequence of the different steps performed by GeoGebra Discovery to confirm a certain statement, as well as a number intending to grade the difficulty or interest of the assertion. The proposal of this assessment measure, involving the comparison of the expression of the thesis (or conclusion) as a combination of the hypotheses, will be developed.
Paper Structure (7 sections, 7 equations, 3 figures)

This paper contains 7 sections, 7 equations, 3 figures.

Table of Contents

  1. Introduction
  2. ShowProof Command
  3. Interestingness
  4. Example 1
  5. Example 2
  6. Example 3
  7. Conclusions

Figures (3)

  • Figure 1: Viewing proof of the Intersection of heights theorem through ShowProof. Initial steps.
  • Figure 2: Viewing proof of the Intersection of heights theorem through ShowProof. Specialized equations, conclusion and difficulty.
  • Figure 3: Automated Geometer: relevant (e.g. Theorem 7, medians intersect at a common point) and trivial (e.g. Theorem 1, midpoint $F$ of $AB$ in the line $AB$, or Theorem 9, midpoint $F$ is equidistant from $A$ and $B$) results.