Search

The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. What follows is a brief description of how the present volume contributes to this enterprise. The 12th International Workshop on Theorem Proving Components for Educational Software(ThEdu'23), was a satellite event of the 29th international Conference on Automated Deduction (CADE 2023), July 1-4, 2023, Rome, Italy. ThEdu'23 was very successful, with one invited talk, by Yves Bertot (Inria, France), "The challenges of using Type Theory to teach Mathematics", and seven regular contributions. An open call for papers was then issued, to which eight contributions were submitted. Seven submissions have been accepted by our reviewers, who jointly produced at least three careful reports on each of the contributions. The resulting revised papers are collected in the present volume. We, the volume editors, hope that this collection of papers will further promote the development of theorem-proving based software, and that it will allow to improve the mutual understanding between computer scientists, mathematicians and stakeholders in education. PC Chairs:Julien Narboux (University of Strasbourg, France); Walther Neuper (JKU, Johannes Kepler University, Linz, Austria); Pedro Quaresma (University of Coimbra, Portugal)

The pursue of what are properties that can be identified to permit an automated reasoning program to generate and find new and interesting theorems is an interesting research goal (pun intended). The automatic discovery of new theorems is a goal in itself, and it has been addressed in specific areas, with different methods. The separation of the "weeds", uninteresting, trivial facts, from the "wheat", new and interesting facts, is much harder, but is also being addressed by different authors using different approaches. In this paper we will focus on geometry. We present and discuss different approaches for the automatic discovery of geometric theorems (and properties), and different metrics to find the interesting theorems among all those that were generated. After this description we will introduce the first result of this article: an undecidability result proving that having an algorithmic procedure that decides for every possible Turing Machine that produces theorems, whether it is able to produce also interesting theorems, is an undecidable problem. Consequently, we will argue that judging whether a theorem prover is able to produce interesting theorems remains a non deterministic task, at best a task to be addressed by program based in an algorithm guided by heuristics criteria. Therefore, as a human, to satisfy this task two things are necessary: an expert survey that sheds light on what a theorem prover/finder of interesting geometric theorems is, and - to enable this analysis - other surveys that clarify metrics and approaches related to the interestingness of geometric theorems. In the conclusion of this article we will introduce the structure of two of these surveys - the second result of this article - and we will discuss some future work., Comment: In Proceedings ADG 2023, arXiv:2401.10725

ADG is a forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools at the intersection between geometry and automated deduction. The conference is held every two years. The previous editions of ADG were held in Hagenberg in 2021 (online, postponed from 2020 due to COVID-19), Nanning in 2018, Strasbourg in 2016, Coimbra in 2014, Edinburgh in 2012, Munich in 2010, Shanghai in 2008, Pontevedra in 2006, Gainesville in 2004, Hagenberg in 2002, Zurich in 2000, Beijing in 1998, and Toulouse in 1996. The 14th edition, ADG 2023, was held in Belgrade, Serbia, in September 20-22, 2023. This edition of ADG had an additional special focus topic, Deduction in Education. Invited Speakers: Julien Narboux, University of Strasbourg, France "Formalisation, arithmetization and automatisation of geometry"; Filip Mari\'c, University of Belgrade, Serbia, "Automatization, formalization and visualization of hyperbolic geometry"; Zlatan Magajna, University of Ljubljana, Slovenia, "Workshop OK Geometry"

The introduction of automated deduction systems in secondary schools face several bottlenecks. Beyond the problems related with the curricula and the teachers, the dissonance between the outcomes of the geometry automated theorem provers and the normal practice of conjecturing and proving in schools is a major barrier to a wider use of such tools in an educational environment. Since the early implementations of geometry automated theorem provers, applications of artificial intelligence methods, synthetic provers based on inference rules and using forward chaining reasoning are considered to be more suited for education proposes. Choosing an appropriate set of rules and an automated method that can use those rules is a major challenge. We discuss one such rule set and its implementation using the geometry deductive databases method (GDDM). The approach is tested using some chosen geometric conjectures that could be the goal of a 7th year class (approx. 12-year-old students). A lesson plan is presented, its goal is the introduction of formal demonstration of proving geometric theorems, trying to motivate students to that goal, Comment: In Proceedings ThEdu'22, arXiv:2303.05360

The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. What follows is a brief description of how the present volume contributes to this enterprise. The 11th International Workshop on Theorem Proving Components for Educational Software (ThEdu'22), was a satellite event of the 8th Federated Logic Conference (FLoC 2022), July 31-August 12, 2022, Haifa, Israel ThEdu'22 was a vibrant workshop, with two invited talk by Thierry Dana-Picard (Jerusalem College of Technology, Jerusalem, Israel) and Yoni Zohar (Bar Ilan University, Tel Aviv, Israel) and four contributions. An open call for papers was then issued, and attracted seven submissions. Those submissions have been accepted by our reviewers, who jointly produced at least three careful reports on each of the contributions. The resulting revised papers are collected in the present volume. The contributions in this volume are a faithful representation of the wide spectrum of ThEdu, ranging from those more focused on the automated deduction research, not losing track of the possible applications in an educational setting, to those focused on the applications, in educational settings, of automated deduction tools and methods. We, the volume editors, hope that this collection of papers will further promote the development of theorem-proving based software, and that it will allow to improve the mutual understanding between computer scientists, mathematicians and stakeholders in education. While this volume goes to press, the next edition of the ThEdu workshop is being prepared: ThEdu'23 will be a satellite event of the 29th international Conference on Automated Deduction (CADE 2023), July 1-4, 2023, Rome, Italy.

The introduction of automated deduction systems in secondary schools face several bottlenecks, the absence of the subject of rigorous mathematical demonstrations in the curricula, the lack of knowledge by the teachers about the subject and the difficulty of tackling the task by automatic means. Despite those difficulties we claim that the subject of automated deduction in geometry can be introduced, by addressing it in particular cases: simple to manipulate by students and teachers and reasonably easy to be dealt by automatic deduction tools. The subject is discussed by addressing four secondary schools geometry problems: their rigorous proofs, visual proofs, numeric proofs, algebraic formal proofs, synthetic formal proofs, or the lack of them. For these problems we discuss a lesson plan to address them with the help of Information and Communications Technology, more specifically, automated deduction tools., Comment: In Proceedings ThEdu'21, arXiv:2202.02144

This EPTCS volume contains the proceedings of the ThEdu'21 workshop, promoted on 11 July 2021, as a satellite event of CADE-28. Due to the COVID-19 pandemic, CADE-28 and all its co-located events happened as virtual events. ThEdu'21 was a vibrant workshop, with an invited talk by Gilles Dowek (ENS Paris-Saclay), eleven contributions, and one demonstration. After the workshop an open call for papers was issued and attracted 10 submissions, 7 of which have been accepted by the reviewers, and collected in the present post-proceedings volume. The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. The volume editors hope that this collection of papers will further promote the development of theorem-proving based software, and that it will collaborate on improving mutual understanding between computer scientists, mathematicians and stakeholders in education.

Mathematical proof is undoubtedly the cornerstone of mathematics. The emergence, in the last years, of computing and reasoning tools, in particular automated geometry theorem provers, has enriched our experience with mathematics immensely. To avoid disparate efforts,the Open Geometry Prover Community Project aims at the integration of the different efforts for the development of geometry automated theorem provers, under a common "umbrella". In this article the necessary steps to such integration are specified and the current implementation of some of those steps is described., Comment: In Proceedings ADG 2021, arXiv:2112.14770

The 9th International Workshop on Theorem-Proving Components for Educational Software (ThEdu'20) was scheduled to happen on June 29 as a satellite of the IJCAR-FSCD 2020 joint meeting, in Paris. The COVID-19 pandemic came by surprise, though, and the main conference was virtualised. Fearing that an online meeting would not allow our community to fully reproduce the usual face-to-face networking opportunities of the ThEdu initiative, the Steering Committee of ThEdu decided to cancel our workshop. Given that many of us had already planned and worked for that moment, we decided that ThEdu'20 could still live in the form of an EPTCS volume. The EPTCS concurred with us, recognising this very singular situation, and accepted our proposal of organising a special issue with papers submitted to ThEdu'20. An open call for papers was then issued, and attracted five submissions, all of which have been accepted by our reviewers, who produced three careful reports on each of the contributions. The resulting revised papers are collected in the present volume. We, the volume editors, hope that this collection of papers will help further promoting the development of theorem-proving-based software, and that it will collaborate to improve the mutual understanding between computer mathematicians and stakeholders in education. With some luck, we would actually expect that the very special circumstances set up by the worst sanitary crisis in a century will happen to reinforce the need for the application of certified components and of verification methods for the production of educational software that would be available even when the traditional on-site learning experiences turn out not to be recommendable.

The geometry automated theorem proving area distinguishes itself by a large number of specific methods and implementations, different approaches (synthetic, algebraic, semi-synthetic) and different goals and applications (from research in the area of artificial intelligence to applications in education). Apart from the usual measures of efficiency (e.g. CPU time), the possibility of visual and/or readable proofs is also an expected output against which the geometry automated theorem provers (GATP) should be measured. The implementation of a competition between GATP would allow to create a test bench for GATP developers to improve the existing ones and to propose new ones. It would also allow to establish a ranking for GATP that could be used by "clients" (e.g. developers of educational e-learning systems) to choose the best implementation for a given intended use., Comment: In Proceedings ThEdu'19, arXiv:2002.11895

This EPTCS volume contains the proceedings of the ThEdu'19 workshop, promoted on August 25, 2019, as a satellite event of CADE-27, in Natal, Brazil. Representing the eighth installment of the ThEdu series, ThEdu'19 was a vibrant workshop, with an invited talk by Sarah Winkler, four contributions, and the first edition of a Geometry Automated Provers Competition. After the workshop an open call for papers was issued and attracted seven submissions, six of which have been accepted by the reviewers, and collected in the present post-proceedings volume. The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favoring software support for this transition by exploiting the power of theorem-proving technologies. The volume editors hope that this collection of papers will further promote the development of theorem-proving-based software, and that it will collaborate on improving mutual understanding between computer mathematicians and stakeholders in education.

The field of geometric automated theorem provers has a long and rich history, from the early AI approaches of the 1960s, synthetic provers, to today algebraic and synthetic provers. The geometry automated deduction area differs from other areas by the strong connection between the axiomatic theories and its standard models. In many cases the geometric constructions are used to establish the theorems' statements, geometric constructions are, in some provers, used to conduct the proof, used as counter-examples to close some branches of the automatic proof. Synthetic geometry proofs are done using geometric properties, proofs that can have a visual counterpart in the supporting geometric construction. With the growing use of geometry automatic deduction tools as applications in other areas, e.g. in education, the need to evaluate them, using different criteria, is felt. Establishing a ranking among geometric automated theorem provers will be useful for the improvement of the current methods/implementations. Improvements could concern wider scope, better efficiency, proof readability and proof reliability. To achieve the goal of being able to compare geometric automated theorem provers a common test bench is needed: a common language to describe the geometric problems; a comprehensive repository of geometric problems and a set of quality measures., Comment: In Proceedings ThEdu'18, arXiv:1903.12402

The 7th International Workshop on Theorem proving components for Educational software (ThEdu'18) was held in Oxford, United Kingdom, on 18 July 2018. It was associated to the conference, Federated Logic Conference 2018 (FLoC2018). The major aim of the ThEdu workshop series was to link developers interested in adapting Computer Theorem Proving (TP) to the needs of education and to inform mathematicians and mathematics educators about TP's potential for educational software. Topics of interest include: methods of automated deduction applied to checking students' input; methods of automated deduction applied to prove post-conditions for particular problem solutions; combinations of deduction and computation enabling systems to propose next steps; automated provers specific for dynamic geometry systems; proof and proving in mathematics education. ThEdu'18 was a vibrant workshop, with one invited talk and six contributions. It triggered the post-proceedings at hand.

The Web Geometry Laboratory (WGL) is a collaborative and adaptive e-learning Web platform integrating a well known dynamic geometry system. Thousands of Geometric problems for Geometric Theorem Provers (TGTP) is a Web-based repository of geometric problems to support the testing and evaluation of geometric automated theorem proving systems. The users of these systems should be able to profit from each other. The TGTP corpus must be made available to the WGL user, allowing, in this way, the exploration of TGTP problems and their proofs. On the other direction TGTP could gain by the possibility of a wider users base submitting new problems. Such information exchange between clients (e.g. WGL) and servers (e.g. TGTP) raises many issues: geometric search - someone, working in a geometric problem, must be able to ask for more information regarding that construction; levels of geometric knowledge and interest - the problems in the servers must be classified in such a way that, in response to a client query, only the problems in the user's level and/or interest are returned; different aims of each tool - e.g. WGL is about secondary school geometry, TGTP is about formal proofs in semi-analytic and algebraic proof methods, not a perfect match indeed; localisation issues, e.g. a Portuguese user obliged to make the query and process the answer in English; technical issues-many technical issues need to be addressed to make this exchange of geometric information possible and useful. Instead of a giant (difficult to maintain) tool, trying to cover all, the interconnection of specialised tools seems much more promising. The challenges to make that connection work are many and difficult, but, it is the authors impression, not insurmountable., Comment: In Proceedings ThEdu'17, arXiv:1803.00722

The 6th International Workshop on Theorem proving components for Educational software (ThEdu'17) was held in Gothenburg, Sweden, on 6 Aug 2017. It was associated to the conference CADE26. Topics of interest include: methods of automated deduction applied to checking students' input; methods of automated deduction applied to prove post-conditions for particular problem solutions; combinations of deduction and computation enabling systems to propose next steps; automated provers specific for dynamic geometry systems; proof and proving in mathematics education. ThEdu'17 was a vibrant workshop, with one invited talk and eight contributions. It triggered the post-proceedings at hand.

The UITP workshop series brings together researchers interested in designing, developing and evaluating user interfaces for automated reasoning tools, such as interactive proof assistants, automated theorem provers, model finders, tools for formal methods, and tools for visualising and manipulating logical formulas and proofs. The twelth edition of UITP took place in Coimbra, Portugal, and was part of the International Joint Conference on Automated Reasoning (IJCAR'16). The workshop consisted of an invited talk, six presentations of submitted papers and lively hands-on session for reasoning tools and their user-interface. These post-proceedings contain four contributed papers accepted for publication after a second round of reviewing after the workshop as well as the invited paper.

The Web Geometry Laboratory, (WGL), is a blended-learning, collaborative and adaptive, Web environment for geometry. It integrates a well known dynamic geometry system. In a collaborative session, exchange of geometrical and textual information between the user engaged in the session is possible. In a normal work session (stand-alone mode), all the geometric steps done by the students are recorded, alongside the navigation information, allowing, in a latter stage, their teachers to "play back" the students sessions, using that info to assert the students level and adjust the teaching strategies to each individual student. Teachers can register and begin using one of the public servers, defining students, preparing materials to be released to the students, open collaborative sessions, etc. Using an action research methodology the WGL system is being developed, validated through case-studies, and further improved, in a cycle where the implementation steps are intertwined with case studies., Comment: CICM 2015, Conference on Intelligent Computer Mathematics (Work-in-Progress track), July 13-17, 2015, Washington DC, USA

Dynamic geometry systems (DGS) have become basic tools in many areas of geometry as, for example, in education. Geometry Automated Theorem Provers (GATP) are an active area of research and are considered as being basic tools in future enhanced educational software as well as in a next generation of mechanized mathematics assistants. Recently emerged Web repositories of geometric knowledge, like TGTP and Intergeo, are an attempt to make the already vast data set of geometric knowledge widely available. Considering the large amount of geometric information already available, we face the need of a query mechanism for descriptions of geometric constructions. In this paper we discuss two approaches for describing geometric figures (declarative and procedural), and present algorithms for querying geometric figures in declaratively and procedurally described corpora, by using a DGS or a dedicated controlled natural language for queries., Comment: 14 pages, 5 figures, accepted at CICM 2014

The "Web Geometry Laboratory" (WGL) project's goal is to build an adaptive and collaborative blended-learning Web-environment for geometry. In its current version (1.0) the WGL is already a collaborative blended-learning Web-environment integrating a dynamic geometry system (DGS) and having some adaptive features. All the base features needed to implement the adaptive module and to allow the integration of a geometry automated theorem prover (GATP) are also already implemented. The actual testing of the WGL platform by high-school teachers is underway and a field-test with high-school students is being prepared. The adaptive module and the GATP integration will be the next steps of this project., Comment: 5 pages; 2 figures; Conferences on Intelligent Computer Mathematics (CICM2013), July 8-12, 2013, University of Bath, Bath, England

With a large number of software tools dedicated to the visualisation and/or demonstration of properties of geometric constructions and also with the emerging of repositories of geometric constructions, there is a strong need of linking them, and making them and their corpora, widely usable. A common setting for interoperable interactive geometry was already proposed, the i2g format, but, in this format, the conjectures and proofs counterparts are missing. A common format capable of linking all the tools in the field of geometry is missing. In this paper an extension of the i2g format is proposed, this extension is capable of describing not only the geometric constructions but also the geometric conjectures. The integration of this format into the Web-based GeoThms, TGTP and Web Geometry Laboratory systems is also discussed., Comment: Conferences on Intelligent Computer Mathematics, CICM 2012, 8.-13. July 2012, Jacobs University, Bremen, Germany. 12 pages 2 figures

The area of geometry with its very strong and appealing visual contents and its also strong and appealing connection between the visual content and its formal specification, is an area where computational tools can enhance, in a significant way, the learning environments. The dynamic geometry software systems (DGSs) can be used to explore the visual contents of geometry. This already mature tools allows an easy construction of geometric figures build from free objects and elementary constructions. The geometric automated theorem provers (GATPs) allows formal deductive reasoning about geometric constructions, extending the reasoning via concrete instances in a given model to formal deductive reasoning in a geometric theory. An adaptative and collaborative blended-learning environment where the DGS and GATP features could be fully explored would be, in our opinion a very rich and challenging learning environment for teachers and students. In this text we will describe the Web Geometry Laboratory a Web environment incorporating a DGS and a repository of geometric problems, that can be used in a synchronous and asynchronous fashion and with some adaptative and collaborative features. As future work we want to enhance the adaptative and collaborative aspects of the environment and also to incorporate a GATP, constructing a dynamic and individualised learning environment for geometry., Comment: In Proceedings THedu'11, arXiv:1202.4535

The THedu'11 workshop received thirteen submissions, twelve of which were accepted and presented during the workshop. For the post-conference proceedings nine submission where received and accepted. The submissions are within the scope of the following points, which have been announced in the call of papers: CTP-based software tools for education; CTP technology combined with novel interfaces, drag and drop, etc.; technologies to access ITP knowledge relevant for a certain step of problem solving; usability considerations on representing ITP knowledge; combination of deduction and computation; formal problem specifications; effectiveness of ATP in checking user input; formats for deductive content in proof documents, geometric constructions, etc; formal domain models for e-learning in mathematics and applications.