Wow, this looks amazing. Do you plan on publishing it on GitHub or something during development when you are done?
[email protected] schrieb am Samstag, 9. Januar 2021 um 06:12:01 UTC+1: > 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/9efaa333-dd50-47bc-a0a0-3e6864643bddn%40googlegroups.com.
