[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

Attachment: signature.asc
Description: This is a digitally signed message part



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