Re: [isabelle] The Incredible Proof Machine



Beautiful work, Joachim! This is definitely useful for teaching, not only high school students, but also beginner college students.
Here is some related work:

https://code.google.com/p/visual-lambda/

All the best, 
  Andrei 

-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Joachim Breitner
Sent: 24 September 2015 15:54
To: isabelle-users
Subject: [isabelle] The Incredible Proof Machine

Hi,

this is slightly off topic and in no way related to the recent discussion about foundations and certification, but I created a new theorem prover.


But first things first:
(The following text is also on my blog at https://www.joachim-breitner.de/blog/682)


In a few weeks, I will have the opportunity to offer a weekend workshop to selected and motivated high school students to a topic of my choice.
My idea is to tell them something about logic, proofs, and the joy of searching and finding proofs, and thegratification of irrevocable truths.

While proving things on paper is already quite nice, it is much more fun to use an interactive theorem prover, such as Isabelle, Coq or
Agda: You get immediate feedback, you can experiment and play around if you are stuck, and you get lots of small successes. Someone once called interactive theorem proving âthe worlds most geekiest videogameâ.

Unfortunately, I donât think one can get high school students without any prior knowledge in logic, or programming, or fancy mathematical symbols, to do something meaningful with a system like Isabelle, so I need something that is (much) easier to use. I always had this idea in the back of my head that proving is not so much about writing text (as in ânormally writtenâ proofs) or programs (as in Agda) or labeled statements (as in Hilbert-style proofs), but rather something involving facts that I have proven so far floating around freely, and way to combine these facts to new facts, without the need to name them, or put them in a particular order or sequence. In a way, Iâm looking for labVIEW wrestled through the Curry-Horward-isomorphism.


So I set out, rounded up a few contributors, implemented this idea, and now I proudly present:

                 The Incredible Proof Machine
                 http://incredible.nomeata.de/

This interactive theorem prover allows you to do perform proofs purely by dragging blocks (representing proof steps) onto the paper and connecting them properly. There is no need to learn syntax, and hence no frustration about getting that wrong. Furthermore, it comes with a number of example tasks to experiment with, so you can simply see it as a challenging computer came and work through them one by one, learning something about the logical connectives and how they work as you go.

For the actual workshop, my plan is to let the students first try to solve the tasks of one session on their own, let them draw their own conclusions and come up with an idea of what they just did, and then deliver an explanation of the logical meaning of what they did.

The implementation is heavily influenced by Isabelle: The software does not know anything about, say, conjunction (â) and implication (â). To the core, everything is but an untyped lambda expression, and when two blocks are connected, it does unification of the proposition present on either side. This general framework is then instantiated by specifying the basic rules (or axioms) in a descriptive manner. It is quite feasible to implement other logics or formal systems on top of this as well.

At this point I must thank Tobias for writing up his pattern unification algorith so nicely back then:
http://www21.in.tum.de/~nipkow/pubs/lics93.html

Another influence of Isabelle is the non-linear editing: You neither have to create the proof in a particular order nor have to manually manage a âproof focusâ. Instead, you can edit any bit of the proof at any time, and the system checks all of it continuously.

As always, I am keen on feedback. Also, if you want to use this for your own teaching or experimenting needs, let me know. We have a mailing list for the project, the code is on GitHub, where you can also file bug reports and feature requests. Contributions are welcome! All aspects of the logic are implemented in Haskell and compiled to JavaScript using GHCJS, the UI is plain hand-written and messy JavaScript code, using JointJS to handle the graph interaction.


Obviously, there is still plenty that can be done to improve the machine. In particular, the ability to create your own proof blocks, such as proof by contradiction, prove them to be valid and then use them  in further proofs, is currently being worked on. And while the page will store your current progress, including all proofs you create, in your browser, it needs better ways to save, load and share tasks, blocks and proofs. Also, weâd like to add some gamification, i.e.
achievements  (âFirst proof by contradictionâ, â50 theorems provenâ), statistics, maybe a âshare theorem on twitterâ button.

Enjoy!
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.