ThEdu'21
ThEdu'21, Programme
Programme — 11 July 2021
All times in Eastern Daylight Time (EDT/USA) (+6 CEST)
| 07:45–08:00 — Welcome and Announcements — Location: ZoomLobb | |||
| 08:00–10:00 — ATPs in Geometry — Chair Walther Neuper | |||
| 8:00–8:30 | slides, video1, video2 | Towards Next Step Guidance in Triangle Construction Problems | Vesna Marinković and Filip Maric |
| 8:30–9:00 | slides,video | Four Geometry Problems to Introduce Automated Deduction in Secondary Schools | Pedro Quaresma and Carlos Reis, |
| 9:00–9:30 | slides,video | Symbolic comparison of geometric quantities in GeoGebra | Zoltán Kovács and Robert Vajda |
| 9:30–10:10 | slides,video | Prooftoys: a proof assistant for beginners (Demonstration) | Crispin Perdue |
| 10:10–10:30 — Coffee Break | |||
| 10:30–12:00 — ATPs
in Geometry & Isabelle, in Education and Accessible — Chair Pedro Quaresma | |||
| 10:30–11:00 | slides,video | Automated Discovery of Geometrical Theorems in GeoGebra | Zoltán Kovács and Jonathan H. Yu |
| 11:00–11:30 | slides,video | Teaching Intuitionistic Propositional Logic Using Isabelle | Jørgen Villadsen, Asta Halkjær From and Patrick Blackburn |
| 11:30–12:00 | slides,video | Make Isabelle Accessible! | Walther Neuper, Klaus Miesenberger, Bernhard Stöger and Reinhard Koutny |
| 12:00–12:30 — Lunch Break | |||
| 12:30–14:00 — Automated Deduction Educational Applications — Chair Walther Neuper | |||
| 12:30–13:00 | slides,video | Learning Theorem Proving by Example — Implementing JavaRes | Adam Pease and Stephan Schulz |
| 13:00–13:30 | slides,video | Evolution of SASyLF 2008-2021 | John Boyland |
| 13:30–14:00 | slides,video | A drag-and-drop proof tactic | Pablo Donato, Benjamin Werner and Pierre-Yves Strub |
| 14:00–14:30 — Coffee Break | |||
| 14:30–16:20 — Invited Talk & Automated Deduction Educational Applications — Chair João Marcos (video) | |||
| 14:30–15:20 | slides,video | Invited Talk — How can we make formal proof teachable? | Gilles Dowek |
| 15:20–15:50 | slides,video | Automated Grading of Automata with ACL2s | Ankit Kumar, Andrew Walter and Panagiotis Manolios |
| 15:50–16:20 | slides,video | Automated Instantiation of Control Flow Tracing Exercises | Clemens Eisenhofer and Martin Riener |
| 16:20–16:40 — Closing and Business Meeting — Chair Pedro Quaresma | |||
| 16:20–16:40 | slides,video | Closing and Business Meeting | ThEdu'21 Chairs |
Programme in PDF format.
