[isabelle] Isabelle (or something else) for Highscool Kids


I might have the opportunity to offer a workshop of 2 days to motivated
and gifted highschool students aged 15-18, and Iâm considering to
bringing the joy of the worldâs most geekiest computer game, i.e.
interactive theorem proving, to them.

Clearly, it is a challenge to simplify and reduce the task enough so
that they can get something done in two days, and both the area (âjustâ
predicate logic? something with naturals? geometry?) and the tools
(Isabelle? Agda? Brunhilde (*g*)? something specialized?) need to be
chosen well.

Has anyone here attempted something of that kind before?

Do you know of theorem provers tailored to, or at lest suitable for,
highschool students? Possibly some where you can build (simple) proofs
by dragging and dropping boxes somehow?


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.