[ThEdu] ThEdu'21 call for participation

[Pedro Quaresma <pedro@mat.uc.pt>]

Dear ThEduers.

ThEdu'21 day, 11 July 2021, is approaching fast.

The CADE 28 registration procedure is now open, please visit the CADE page to register.

"Regular participant" - if you want to participate in the main conference + workshops + tutorials

"Workshop and Tutorials only" - if you do not want to attend the main conference.

ThEdu’21, Theorem Proving Components for Educational Software

Programme — 11 July 2021

All sessions (except the Welcome session) are in ZoomRoom 1 (more info about that as soon as possible).

All time-slots for presentations assume a 10min final slot for Q&A.

All times in Eastern Daylight Time (EDT/USA) (+6 CEST)

   07:45-08:00 --- Welcome and Announcements --- Location: ZoomLobby
   08:00-10:00 --- ATPs in Geometry 

   8:00–8:30   Towards Next Step Guidance in Triangle Construction Problems                 Vesna Marinković and Filip Maric
   8:30–9:00   Four Geometry Problems to Introduce Automated Deduction in Secondary Schools Pedro Quaresma and Carlos Reis,
   9:00–9:30   Symbolic comparison of geometric quantities in GeoGebra                      Zoltán Kovács and Robert Vajda
   9:30–10:10  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 
                                                                                   
   10:30–11:00  Automated Discovery of Geometrical Theorems in GeoGebra                     Zoltán Kovács and Jonathan H. Yu
   11:00–11:30  Teaching Intuitionistic Propositional Logic Using Isabelle                  Jørgen Villadsen, Asta Halkjær From and Patrick Blackburn
   11:30–12:00  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 
                                                                                    
                                                                                               
   12:00–12:30  Learning Theorem Proving by Example — Implementing JavaRes                  Adam Pease and Stephan Schulz
   13:00–13:30  Evolution of SASyLF 2008-2021                                               John Boyland
   13:30–14:00  A drag-and-drop proof tactic                                                Pablo Donato, Benjamin Werner and Pierre-Yves Strub
                                                                                               
                                                                                                 
   14:00-14:20 --- Coffee Break                                                                              
   14:20-16:10 --- Invited Talk & Automated Deduction Educational Applications 

   14:20–15:10  Invited Talk — How can we make formal proof teachable?                      Gilles Dowek
   15:10–15:40  Automated Grading of Automata with ACL2s                                    Ankit Kumar, Andrew Walter and Panagiotis Manolios
   15:40–16:10  Automated Instantiation of Control Flow Tracing Exercises                   Clemens Eisenhofer and Martin Riener

Cheers,

-- 

At\'e breve;Deica Logo;\`A bient\^ot;See you later;Vidimo se;A tra poco;Do zobaczenia

Professor Pedro Quaresma
Mathematics Departament, Science and Technology Faculty
University of Coimbra
P-3001-454 COIMBRA, PORTUGAL
Elec. mail: pedro@mat.uc.pt
webpage: http://www.mat.uc.pt/~pedro/
phone: +351 239 791 137; fax: +351 239 832 568