论文标题
会议记录第9届国际定理研讨会证明了教育软件的组成部分
Proceedings 9th International Workshop on Theorem Proving Components for Educational Software
论文作者
论文摘要
第9届国际教育软件定理组件（THEDU'20）的国际研讨会定于6月29日举行，作为巴黎的IJCAR-FSCD 2020联合会议的卫星。 不过，19009年的大流行令人惊讶，主要会议是虚拟化的。 由于担心在线会议不会允许我们的社区完全复制Thedu倡议的通常面对面网络机会，因此Thedu的指导委员会决定取消我们的研讨会。鉴于我们中的许多人已经计划和工作了，因此我们认为Thedu'20仍然可以生活在EPTCS卷的形式中。 EPTC与我们同意，认识到这种非常奇特的情况，并接受了我们组织特刊的提议，并提交给Thedu'20的论文。 然后发出了公开的论文呼吁，并吸引了五份意见书，所有这些都被我们的审稿人接受，他们对每项捐款都仔细报告了。 在本卷中收集了由此产生的修订论文。我们的数量编辑，希望这些论文集将有助于进一步促进基于定理的软件的开发，并将合作，以提高计算机数学家和教育利益相关者之间的相互了解。 幸运的是，我们实际上希望，一个世纪内最严重的卫生危机所设定的非常特殊的情况将碰巧需要使用经过认证的组件和生产教育软件的验证方法，即使传统的现场学习经验也可以使用，这也是不可推荐的。
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.
