Exploring Quadrilaterals: An Interactive Task for 7th Grade Students Using GeoGebra Classroom

Using a Dynamic Geometry System (DGS) students can engage in a dynamic learning process that allows them to experiment, create strategies, make conjectures, argue, and deduce mathematical properties. A DGS enables the introduction of proofs, by providing visual aids. The proof of the conjectures made emerges as the next step towards formalising and understanding the contents covered and the introduction of automated deduction systems at schools can be an added value. The implementation of automated deduction systems in schools faces several challenges, such as curriculum-issues, teacher knowledge and the discrepancy between automated theorem provers and traditional practices of proving in schools. Synthetic provers based on a set of inference rules and forward chaining reasoning may provide a possible help to these challenges. With the aim of introducing formal proofs and inspiring students towards this goal, a geometric conjecture was chosen for 7th grade students to engage with, based on a rule set discussed in a previous work, "A rule based theorem prover: an introduction to proofs in secondary schools". The study also aimed to showcase the application of a Geometry Automated Theorem Prover within the classroom setting. A sequence of tasks was created for students to complete using GeoGebra Classroom. In the first phase, they were asked to identify quadrilaterals, construct a parallelogram, and measure sides and angles until they formulated a conjecture, which was strengthened by the dynamic possibility of changing the constructed parallelogram. In the second phase, the students were provided with four rules and were asked to justify their results using these rules. By the end of these justifications, the students had a complete proof of the initial conjecture. A short video of the proof made using JGEx (Java Geometry Expert) was also shown to the students.