Gamifying mathematics (an interactive tutorial for sequent calculus)(logitext.ezyang.scripts.mit.edu)
logitext.ezyang.scripts.mit.edu
Gamifying mathematics (an interactive tutorial for sequent calculus)
http://logitext.ezyang.scripts.mit.edu/logitext.fcgi/tutorial?
3 comments
The linked book by Pierce is pretty fantastic as well. http://www.cis.upenn.edu/~bcpierce/sf/
I've been working on a similar project for high school algebra. Mine isn't as far along, so it's been nice to see some validation on my ideas, as well as get some thoughts on how I would improve.
How do you make contraction happen? I don't see a button for it.
We do contraction on implication-left automatically, and only have it as an option for forall-left and exists-right, since it's not a useful notion for the other operators.