This is cool, but I think the UI needs a little work.
For example my natural inclination is to click the output of one logic block and click the input of the next. As opposed to dragging the output to the input. Luckily I have a mouse, but this would be annoying on a laptop. The single click doesn't make sense to me because you're not redirecting output to output, which is what happens when you just click (can be hard to delete line)
What I _DO_ like is that they start with easy examples and do a good job of working you into more complex ones. Makes things really intuitive and I think this is a good tool for teaching people.
My natural inclination in the first problem (A->A) was to drag the output A onto the input A (or vice versa), and when nothing then happened I couldn't see how to fix things. Reading the info link didn't clear that up; I had to read the journal paper and skim for a completed example there.
That actually what I did first too (well, drag output to input), and was really irritated that they didn't line up. But next step was to click. Took a few tries to realize I could drag.
I was really confused about "local hypotheses" for a minute there. In session 2, you get two blocks for working with implications.
One is a modus ponens block -- given the two inputs (X -> Y) and (X), it produces the output (Y).
The other is a block for positing assumptions ("local hypotheses"). In the block selection menu, it has an ordinary output of (X -> Y). It has a notch in the top with an output of (X) on the left and an input of (Y) on the right.
The function of this block, as shown by the ordinary output, is to prove statements of the form (X -> Y). For this purpose, it gives you a free output of X, but every path you send that X through must eventually either be abandoned or come back to the matching Y input in its notch.
The X will magically become the variable you need when connected to the appropriate input of a modus ponens block.
This was a fun puzzle, but I came to a roadblock here too.
I have to confess I'm confused by what I believe might be the "local hypothesis block" mentioned above. The confusion is somewhat greater because the blocks don't seem to have any attached name or description, so it's not clear what they're meant to be doing.
Up until task 5 in session 2, all the solutions are pretty trivial. But I can't work out what sort of wiring that block implies (for the record, the task is "given (A->B, B->C), prove (A->C)").
It's really not clear to me what the "notch" at the top of that block implies, or how it might be used.
I think there should be at least one "hand-holding" solution for the first use of each block type. Even the papers linked to don't describe the intended semantics of each block.
OK, replying to myself for future reference. I found the answer here: https://youtu.be/0GeJdTTzaDo (incidentally, that series of videos seems to have solutions for most of these problems).
The answer is that the left and right side of the notch holds local equivalents to the global "given X, prove Y" connectors. You can use the left side of the notch as an input, and you can connect that up through the global blocks to prove the hypothesis.
That was non-obvious! Also, the technique of connecting the output first and making connections to nothing to see what the implied proposition is was very useful - I should have thought of that.
One is for a proof by cases; it accepts a disjunction ("or") as input, gives you a local branch for each disjoined option, and hopes you'll show that each branch individually proves P. Then the block globally proves P. This one was intuitive to me.
One is for instantiating variables from existential quantifiers. If you send ∃x.P(x) into that block's global input, you will get P(c), where c is a constant, coming out of that block's local output. You're supposed to prove an expression that does not involve c, send that to local input, and get it back out of global output.
As far as I can tell, this is done for reasons of convenient implementation. Mathematically, the notch shouldn't be there at all -- you should just be able to hook up ∃x.P(x) to global input, and get P(c) on global output. But I think the tool author wants to think of c as being a variable which is scoped inside the ∃-instantiation block and can't exist outside it.
I've worked on a similar project (https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html), where the interface allows only for backwards proofs. The only action allowed is to click a proof rule to be applied next, and the proof is presented in Fitch-like notation. Currently limited to propositional logic (not first-order).
Very fun, but I've never seen proofs in this format. I would expect to see the "prerequisites" on the top of the line and the "thing that follows" below. e.g.
This is really cool! And awesome that (anecdotally) it seems to have been an effective tool for teaching high school students about logic and proof. Excited to dig in and learn more at some point about how this relates to formal proof assistants.
For example my natural inclination is to click the output of one logic block and click the input of the next. As opposed to dragging the output to the input. Luckily I have a mouse, but this would be annoying on a laptop. The single click doesn't make sense to me because you're not redirecting output to output, which is what happens when you just click (can be hard to delete line)
What I _DO_ like is that they start with easy examples and do a good job of working you into more complex ones. Makes things really intuitive and I think this is a good tool for teaching people.