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



In my opinion, pure predicate logic will come across as boring and dry. The most understandable problems would be puzzles in propositional logic, for which SAT solvers are much more appropriate than any interactive tool.

I suggest something from recreational mathematics, such as Fibonacci numbers and basic facts about them. If these students are familiar with induction, then you could prove some simple facts about the Fibonacci numbers. Possible alternatives include the GCD function and Ackermannâs function.

An alternative might be to teach a tiny bit of functional programming, along with proofs.

In both cases, you may be able to get away with equational logic, especially through the magic of assumes/shows.

Larry Paulson


> On 18 Jun 2015, at 13:32, Joachim Breitner <breitner at kit.edu> wrote:
> 
> Hi,
> 
> 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?
> 
> Thanks,
> Joachim
> 
> -- 
> Dipl.-Math. Dipl.-Inform. Joachim Breitner
> Wissenschaftlicher Mitarbeiter
> http://pp.ipd.kit.edu/~breitner





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