*To*: Joachim Breitner <breitner at kit.edu>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] The Incredible Proof Machine*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Fri, 25 Sep 2015 11:13:57 +0200*Cc*: Vincent van Oostrom <Vincent.van-Oostrom at uibk.ac.at>, Julian Nagele <julian.nagele at uibk.ac.at>*In-reply-to*: <1443106448.1431.17.camel@kit.edu>*References*: <1443106448.1431.17.camel@kit.edu>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.2.0

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 Dear Joachim, nice work! This reminds me of two things: 1) I saw something similar (?) a few month ago (IIRC for plain propositional logic and implemented via first-order unification), which was the result of a student project supervised by Vincent van Oostrom (who I CC'ed). AFAIK it is only available as non-free iPhone app. Anyway, maybe there are ideas that could be exchanged? 2) Since you mentioned the nice paper by Tobias (on higher-order pattern unification). Did you also implement the "devar" optimization of the same paper? Just recently, Julian Nagele (a PhD student in our group; who I also CC'ed), stumbled upon a problem with "devar" when implementing the same algorithm. I do not remember the details (maybe Julian could comment), only that a little bit of hg-digging revealed the following changeset: changeset: 12232:ff75ed08b3fb user: berghofe date: Mon Nov 19 17:34:02 2001 +0100 summary: Replaced devar by Envir.head_norm (referring to src/Pure/pattern.ML) I'm curios to whether others already had a similar experience with "devar" and what the intention behind this change was? cheers chris On 09/24/2015 04:54 PM, Joachim Breitner wrote: > 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 > -----BEGIN PGP SIGNATURE----- Version: GnuPG v2 iQIcBAEBCAAGBQJWBRBEAAoJECdPcHF8FDHN7WoP/R0tcgBMqAPHcvLcWfHbV10A rYp2pucDYGzlbwmSK8AwK10bZ+UkrIwCESFHhxYyZABe/RyM8KbfgIQarcez1EkO O6RPOHnCqPNH+PDuT7rvLERqOM6afmNktf3o7p45xcR63enHkvGiNnVJ2Ur7z5Li XXQwyzypr+G/2kjFLu3+ajy7P1mNpD8xBzz7Y4E3OH2+fX7IZVT8tLIcT0hGf0ku 0ey592j+Dy6c0s9H5q2GqyvPhWsBqjAdkx5UHwLAtBx1mguVLSXsLlyymdMOx+dT TKeHLRvvVMW7sSW96uZ1P1902LaQm4YCD5HN9ZDg0LGw7V1Qco5lT1S4BCzDER4u tJPL+7t+LEHQZr5dSJW4kpQ+aZQfNoNBAYAIztm1bhgObNgWd3N38CtGzCFll3uE HU5ueLEdkjEGWgyOeCvjO4Ztono3xUuYXUdgYy0mrEGYmERTyVEM5Fj2ml6Dw/jp nFKtXJKqmrzSGzSEEfF6YLFEOhI8CBZrCTLcDMfEWWnRdTLKRfdumQwMR0tvJgmB YsBE3FkkY+UNIpZA53jgPZM05FMNcBtMQpBV/G29gl6fRZRbtEiZVtWJgeqQa4F0 TpEZ26qNPFZBJMjI0ZBM1Df1F8yUgA4f48pekMVU4TGhfGrXX5UtB4AavdPEh1Ec luroBAze10VYXH6FszXd =1iKD -----END PGP SIGNATURE-----

**Follow-Ups**:**Re: [isabelle] The Incredible Proof Machine***From:*Joachim Breitner

**References**:**[isabelle] The Incredible Proof Machine***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] find_consts does not find constants from BNF package
- Next by Date: Re: [isabelle] The Incredible Proof Machine
- Previous by Thread: Re: [isabelle] The Incredible Proof Machine
- Next by Thread: Re: [isabelle] The Incredible Proof Machine
- Cl-isabelle-users September 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list