Gamifying propositional logic: QED, an interactive textbook
terrytao.wordpress.com
Gamifying propositional logic: QED, an interactive textbook
1–10 of 22 posts
Re: Gamifying propositional logic: QED, an interactive textbook
#2There's earlier, non computer game precedence in To Mock a Mockingbird, which I feel is similar in spirit.
Nice find OP
Re: Gamifying propositional logic: QED, an interactive textbook
#39.3(d) was a real pain until I thought about how I'd write a function with type `(Either a b, Either a c) -> Either a (b, c)`. Before that, I kept wanting a negation operator.
(EDIT: Looks like some of the exercises are getting shuffled between versions -- 9.3(d) is the one I meant as of v1.2, but that might change over time. At least the type signature is a clue about which one I mean.)
Re: Gamifying propositional logic: QED, an interactive textbook
#4Reminds me quite a bit of this, which also includes FOL: http://proofs.openlogicproject.org/
Re: Gamifying propositional logic: QED, an interactive textbook
#5See also "The Markable Mark": http://www.markability.net/
It's an introduction to logic using George Spencer-Brown's Laws of Form notation.
Re: Gamifying propositional logic: QED, an interactive textbook
#6Last time I spent some time trying to learn mathematical logic I realized that logic texts could benefit from syntax coloring of various languages involved (e.g., metalanguage, object language, logic symbols vs non-logic math symbols, etc, etc).
I'm not sure if this is considered as pedagogically beneficial, and/or feasible without interactivity (on a cursory glance, it doesn't look like Terence Tao has given any importance to coloring in this project).
Re: Gamifying propositional logic: QED, an interactive textbook
#7This is a very nice game/textbook!
I'd love to see some additional features:
- I'm currently at the excercise 9.1, and this far PUSH is always the only operation you can do when dragging from an outer scope to an inner one. Seems pretty fundamental. (To the extent that explicit mentions of "pushing" is not even normally mentioned in textual proofs?) Could this be streamlined somehow, for example applying PUSH automatically just with the drag & drop operation from outer to inner scope?
- Instead of a linear "achievement history", keep records of all produced proofs for each lemma. Highlight the one with the smallest amount of "rules".
- It seems to allow circular proofs by default. Surely this can be detected using a dependency graph?
- Speaking of dependency graphs, I'd love to explore reverse mathematics using this kind of an interactive tool. Maybe add some challenge by counting not only the amount of rules, but amount of axioms/basic rules of inference used, and counting also the size of the whole dependency graph of each proof. Maybe there could be separate record-keeping for different sets of axioms.
Re: Gamifying propositional logic: QED, an interactive textbook
#8Related: Nicky Case (whose website you really should check out) is currently organizing an Explorables Jam until the nineteenth of August[0][1].
Re: Gamifying propositional logic: QED, an interactive textbook
#99.3(d) was a real pain until I thought about how I'd write a function with type `(Either a b, Either a c) -> Either a (b, c)`. Before that, I kept wanting a negation operator. (EDIT: Looks like some of the exercises are getting shuffled between versions -- 9.3(d) is the one I meant as of v1.2, but that might change over time. At least the type signature is a clue about which one I mean.)
I'm totally stuck. I would write an exhaustive pattern match to implement that function, but I have no clue how to do that in logic, without using negation.
Re: Gamifying propositional logic: QED, an interactive textbook
#10Shameless plug: I have created an Android game for learning propositional logic that's probably more suitable for younger audiences.
Source code: https://github.com/stefanhaustein/emojic (the page has a playstore link which has screenshots).
Have fun competing with your kids O:)