-
Interactive Formal Specification for Mathematical Problems of Engineers
Authors:
Walther Neuper
Abstract:
The paper presents the second part of a precise description of the prototype that has been developed in the course of the ISAC project over the last two decades. This part describes the "specify-phase", while the first part describing the "solve-phase" is already published.
In the specify-phase a student interactively constructs a formal specification. The ISAC prototype implements formal spec…
▽ More
The paper presents the second part of a precise description of the prototype that has been developed in the course of the ISAC project over the last two decades. This part describes the "specify-phase", while the first part describing the "solve-phase" is already published.
In the specify-phase a student interactively constructs a formal specification. The ISAC prototype implements formal specifications as established in theoretical computer science, however, the input language for the construction avoids requiring users to have knowledge of logic; this makes the system useful for various engineering faculties (and also for high school).
The paper discusses not only ISAC's design of the specify-phase in detail, but also gives a brief introduction to implementation with the aim of advertising the re-use of formal frameworks (inclusive respective front-ends) with their generic tools for language definition and their rich pool of software components for formal mathematics.
△ Less
Submitted 8 April, 2024;
originally announced April 2024.
-
Proceedings 12th International Workshop on Theorem proving components for Educational software
Authors:
Julien Narboux,
Walther Neuper,
Pedro Quaresma
Abstract:
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 W…
▽ More
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)
△ Less
Submitted 4 April, 2024;
originally announced April 2024.
-
Towards an Accessible Mathematics Working Environment Based on Isabelle/VSCode
Authors:
Klaus Miesenberger,
Walther Neuper,
Bernhard Stöger,
Makarius Wenzel
Abstract:
The paper collects preparatory work for interdisciplinary collaboration between three partners, between (1) expertise in improving accessibility of studies for impaired individuals, (2) expertise in develo** educational mathematics software and (3) expertise in designing and implementing interactive proof assistants.
The cooperation was started with the goal to develop an accessible mathemat…
▽ More
The paper collects preparatory work for interdisciplinary collaboration between three partners, between (1) expertise in improving accessibility of studies for impaired individuals, (2) expertise in develo** educational mathematics software and (3) expertise in designing and implementing interactive proof assistants.
The cooperation was started with the goal to develop an accessible mathematics working environment for education with reasonable efforts. The start was triggered by the lucky discovery that the upcoming Isabelle/VSCode is greatly accessible for blind users without further impairments; this is envisaged as the project's target group.
Technical details are described to an extent necessary to understand essential details of efforts required for development. A survey of demand from practice of education with respect to (1) and (2) leads to a vision for educational math software, which necessarily is sketchy but suffices to guide development and which shall invite experts in didactics of mathematics to collaborate.
△ Less
Submitted 10 March, 2023;
originally announced March 2023.
-
Proceedings 11th International Workshop on Theorem Proving Components for Educational Software
Authors:
Pedro Quaresma,
João Marcos,
Walther Neuper
Abstract:
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 Wor…
▽ More
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.
△ Less
Submitted 9 March, 2023;
originally announced March 2023.
-
Proceedings 10th International Workshop on Theorem Proving Components for Educational Software
Authors:
João Marcos,
Walther Neuper,
Pedro Quaresma
Abstract:
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 pape…
▽ More
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.
△ Less
Submitted 2 February, 2022;
originally announced February 2022.
-
Lucas-Interpretation on Isabelle's Functions
Authors:
Walther Neuper
Abstract:
Software tools of Automated Reasoning are too sophisticated for general use in mathematics education and respective reasoning, while Lucas-Interpretation provides a general concept for integrating such tools into educational software with the purpose to reliably and flexibly check formal input of students. This paper gives the first technically concise description of Lucas-Interpretation at the oc…
▽ More
Software tools of Automated Reasoning are too sophisticated for general use in mathematics education and respective reasoning, while Lucas-Interpretation provides a general concept for integrating such tools into educational software with the purpose to reliably and flexibly check formal input of students. This paper gives the first technically concise description of Lucas-Interpretation at the occasion of migrating a prototype implementation to the function package of the proof assistant Isabelle. The description shows straightforward adaptations of Isabelle's programming language and shows, how simple migration of the interpreter was, since the design (before the function package has been introduced to Isabelle) recognised appropriateness of Isabelle's terms as middle end. The paper gives links into the code in an open repository as invitation to readers for re-using the prototyped code or adopt the general concept. And since the prototype has been designed before the function package was implemented, the paper is an opportunity for recording lessons learned from Isabelle's development of code structure.
△ Less
Submitted 29 October, 2020;
originally announced October 2020.
-
Proceedings 9th International Workshop on Theorem Proving Components for Educational Software
Authors:
Pedro Quaresma,
Walther Neuper,
João Marcos
Abstract:
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…
▽ More
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.
△ Less
Submitted 27 October, 2020;
originally announced October 2020.
-
Proceedings 8th International Workshop on Theorem Proving Components for Educational Software
Authors:
Pedro Quaresma,
Walther Neuper,
João Marcos
Abstract:
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 f…
▽ More
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.
△ Less
Submitted 26 February, 2020;
originally announced February 2020.
-
Technologies for "Complete, Transparent & Interactive Models of Math" in Education
Authors:
Walther Neuper
Abstract:
A new generation of educational mathematics software is being shaped in ThEdu and other academic communities on the side of computer mathematics. Respective concepts and technologies have been clarified to an extent, which calls for cooperation with educational sciences in order to optimise the new generation's impact on educational practice. The paper addresses educational scientists who want to…
▽ More
A new generation of educational mathematics software is being shaped in ThEdu and other academic communities on the side of computer mathematics. Respective concepts and technologies have been clarified to an extent, which calls for cooperation with educational sciences in order to optimise the new generation's impact on educational practice. The paper addresses educational scientists who want to examine specific software features and estimate respective effects in STEM education at universities and subsequently at high-school. The key features are characterised as a "complete, transparent and interactive model of mathematics", which offers interactive experience in all relevant aspects in doing mathematics. Interaction uses several layers of formal languages: the language of terms, of specifications, of proofs and of program language, which are connected by Lucas-Interpretation providing "next-step-guidance" as well as providing prover power to check user input. So this paper is structured from the point of view of computer mathematics and thus cannot give a serious description of effects on educational practice -- this is up to collaboration with educational science; such collaboration is prepared by a series of questions, some of which are biased towards software usability (and mainly to be solved by computer mathematicians) and some of which are biased towards genuine research in educational sciences.
△ Less
Submitted 1 April, 2019;
originally announced April 2019.
-
Proceedings 7th International Workshop on Theorem proving components for Educational software
Authors:
Pedro Quaresma,
Walther Neuper
Abstract:
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 mathemat…
▽ More
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.
△ Less
Submitted 29 March, 2019;
originally announced March 2019.
-
Prototy** "Systems that Explain Themselves" for Education
Authors:
Alan Krempler,
Walther Neuper
Abstract:
"Systems that Explain Themselves" appears a provocative wording, in particular in the context of mathematics education -- it is as provocative as the idea of building educational software upon technology from computer theorem proving. In spite of recent success stories like the proofs of the Four Colour Theorem or the Kepler Conjecture, mechanised proof is still considered somewhat esoteric by ma…
▽ More
"Systems that Explain Themselves" appears a provocative wording, in particular in the context of mathematics education -- it is as provocative as the idea of building educational software upon technology from computer theorem proving. In spite of recent success stories like the proofs of the Four Colour Theorem or the Kepler Conjecture, mechanised proof is still considered somewhat esoteric by mainstream mathematics. This paper describes the process of prototy** in the ISAC project from a technical perspective. This perspective depends on two moving targets: On the one side the rapidly increasing power and coverage of computer theorem provers and their user interfaces, and on the other side potential users: What can students and teachers request from educational systems based on technology and concepts from computer theorem proving, now and then? By the way of describing the process of prototy** the first comprehensive survey on the state of the ISAC prototype is given as a side effect, made precise by pointers to the code and by citation of all contributing theses.
△ Less
Submitted 4 March, 2018;
originally announced March 2018.
-
Proceedings 6th International Workshop on Theorem proving components for Educational software
Authors:
Pedro Quaresma,
Walther Neuper
Abstract:
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…
▽ More
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.
△ Less
Submitted 2 March, 2018;
originally announced March 2018.
-
Automated Generation of User Guidance by Combining Computation and Deduction
Authors:
Walther Neuper
Abstract:
Herewith, a fairly old concept is published for the first time and named "Lucas Interpretation". This has been implemented in a prototype, which has been proved useful in educational practice and has gained academic relevance with an emerging generation of educational mathematics assistants (EMA) based on Computer Theorem Proving (CTP).
Automated Theorem Proving (ATP), i.e. deduction, is the mos…
▽ More
Herewith, a fairly old concept is published for the first time and named "Lucas Interpretation". This has been implemented in a prototype, which has been proved useful in educational practice and has gained academic relevance with an emerging generation of educational mathematics assistants (EMA) based on Computer Theorem Proving (CTP).
Automated Theorem Proving (ATP), i.e. deduction, is the most reliable technology used to check user input. However ATP is inherently weak in automatically generating solutions for arbitrary problems in applied mathematics. This weakness is crucial for EMAs: when ATP checks user input as incorrect and the learner gets stuck then the system should be able to suggest possible next steps.
The key idea of Lucas Interpretation is to compute the steps of a calculation following a program written in a novel CTP-based programming language, i.e. computation provides the next steps. User guidance is generated by combining deduction and computation: the latter is performed by a specific language interpreter, which works like a debugger and hands over control to the learner at breakpoints, i.e. tactics generating the steps of calculation. The interpreter also builds up logical contexts providing ATP with the data required for checking user input, thus combining computation and deduction.
The paper describes the concepts underlying Lucas Interpretation so that open questions can adequately be addressed, and prerequisites for further work are provided.
△ Less
Submitted 22 February, 2012;
originally announced February 2012.
