Hello, I'm experimenting with using visual blocks to represent and edit proofs using the morphic.js framework by Jens Mönig <https://github.com/jmoenig/morphic.js>. I don't have a whole lot at the moment, but here's a screenshot of a nearly-complete proof of ( -. p -> ( p -> q ) ) from axioms to demonstrate what I have so far:
[image: image.png] Each block represents a theorem. The slots represent mandatory hypotheses, and the block itself exposes the theorem's assertion. For this picture, I color-coded ax-1 as red, ax-2 as green, and ax-3 as blue. All blocks will unify their expressions when connected to a slot, updating their own label to match the new expression. The lowest block is just a pass-through block that exposes a "wff" slot in addition to the "|-" slot. It's used here to give the wff variables names, since they would otherwise just show up as "?" (like in the disconnected red block). This project is still very early in development, but I hope that it will become an intuitive way to experiment with theorem proving. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAJqce9aBBKGg-ch2C_KLwJyraLH7p3Wb0MQ0JH5P6x-grL7G9w%40mail.gmail.com.
