Re: [isabelle] Isabelle (or something else) for Highscool Kids
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
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