Email Gateway (Aug 22 2022 at 10:14): Email Gateway (Aug 22 2022 at 10:14):From: Joachim Breitner <breitner@kit.edu>
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
signature.asc
Email Gateway (Aug 22 2022 at 10:14):From: "Elsa L. Gunter" <egunter@illinois.edu>
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.
---Elsa
Email Gateway (Aug 22 2022 at 10:14):From: Larry Paulson <lp15@cam.ac.uk>
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
Last updated: Apr 16 2024 at 08:18 UTC