Re: [isabelle] The Incredible Proof Machine

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?



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
> 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
> 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: 
> 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
Version: GnuPG v2


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