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

Dear Joachim,
You might take a look at Tarski's World, which has been used successfully for a similar audience. It gives an introduction to first-order logic. It might give you some ideas how to organize things.

On 6/18/15 7:32 AM, Joachim Breitner wrote:

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?


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