Email Gateway (Aug 22 2022 at 11:18): Email Gateway (Aug 22 2022 at 11:18):From: Joachim Breitner <breitner@kit.edu>
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
signature.asc
Email Gateway (Aug 22 2022 at 11:18):From: Peter Lammich <lammich@in.tum.de>
Nice work.
Just one experience when I played around with it, which puzzled me, and
might severely puzzle your students: I tried A&B&C ==> A&C, my attempt
is attached.
As I did not know whether & binds to left or right, I ended up attaching
the line to the wrong exit. But then, I got an error on the line from
the start, which was fine previously. I.e., when I attach something to a
block, I may get an error at a seemingly unrelated point.
Moreover, if I have something like
A&B&C ---> (dest-AND)
I would like to "see" which propositions are available at the outputs.
-- Peter
incredible-proof.svg
Email Gateway (Aug 22 2022 at 11:19):From: Joachim Breitner <breitner@kit.edu>
Dear Peter,
Am Donnerstag, den 24.09.2015, 17:54 +0200 schrieb Peter Lammich:
Just one experience when I played around with it, which puzzled me,
and might severely puzzle your students: I tried A&B&C ==> A&C, my attempt
is attached.As I did not know whether & binds to left or right, I ended up
attaching the line to the wrong exit. But then, I got an error on the
line from the start, which was fine previously. I.e., when I attach
something to a block, I may get an error at a seemingly unrelated
point.
Right. One of my ideas is to keep track of the order in which
connections have been added (or been changed), and apply unification in
that order. In fact, I think I forgot that I planned to do this, so I
better create an issue for it:
https://github.com/nomeata/incredible/issues/26
Moreover, if I have something like
A&B&C ---> (dest-AND)I would like to "see" which propositions are available at the
outputs.
You can always “pull out” a connection (without connecting it to
something else) and see what’s on it. But it would be more convenient
to see something right away; this is also planned:
https://github.com/nomeata/incredible/issues/24
Greetings,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 11:19):From: Christian Sternagel <c.sternagel@gmail.com>
-----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
-----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-----
Email Gateway (Aug 22 2022 at 11:19):From: Joachim Breitner <breitner@kit.edu>
Dear Christian,
Are you referring to “§9 Minimizing new variables” in the paper? Since
this seems to be part of the ML code in
http://www21.in.tum.de/~nipkow/pubs/lics93-alpha.ML which I based my
implementation on, I also have that. If there is anything wrong with
it, I’d like to know of course!
Thanks,
Joachim
signature.asc
Email Gateway (Aug 22 2022 at 11:19):From: Christian Sternagel <c.sternagel@gmail.com>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256
Dear Joachim,
Sorry, I really can't remember the details, but I'm pretty sure that
it was just about the concrete implementation of the "devar" function
(section 6; so it should not be related to section 9).
I hope that Julian will fill in the details at some point ;)
cheers
chris
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2
iQIcBAEBCAAGBQJWBTfoAAoJECdPcHF8FDHN9JcQALciOoEOX4B5oATc3kPTqHMU
KkM+0RqJmzgJz74SmqqkEtQjm/ecfGP8CYTl3g8cctHjiJD/V1+IFi7whc8o/75I
gQ77hh6g7UBx+h8Gv4r8RLonBN59A4FKv7iBmzy0T9PsAAL6uhSlGs6Andgmj4oP
90yMKvC/7wa5Ub0YLVS8K8MPgppYCKh+oTi+xIf9nHzKQRKAVLgu5ot/whF9is3C
uniP428jmryLElJlM+LHm87PMmvGxd0XaRG9LpMRa9NxD0r17dOEG1RXNhVdxcjj
ixHKP8R7nTQD6VwBxMwxBgY4NvbLCZWQT7y/Agmitg3CF9zdA89tZKt2EX8Cqlnr
MSg8yjH8oiW3G6/2msAep9hiqXylgtJNqnrgW6DjorFjLkLNXWLmwdz6TT1mHg24
/+Cbf2hHUZJERdK/qZ48TOGVaI66x1Szf5JXOwK4McBjDLtBgBe2lFMh4aFQ6HQF
9XVF0tEG2pC170JBscbSuXioeNdUF+u6ggqP0vDKDOS/I8kzWgdd5FSqCC1BQBth
iLSlTlj8c76BE4Zzu+mb7mWth63qv3RbKU4PQw8cmYSEBDRa4tYWPY1OvO+udSOG
AXsc5+GOw3BBwMFyUS9Agw8PAsv6rJEhv4OXaiYGi8ZyMZu8pRDCMNA2IRosLJxs
YTCvUwAlaMQ0zL4re4DR
=5Wgq
-----END PGP SIGNATURE-----
Email Gateway (Aug 22 2022 at 11:19):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
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
Last updated: Apr 25 2024 at 12:23 UTC
