5 ms·

The Incredible Proof Machine (2016)

79 points by chewxy 8y ago

godelski 8y ago
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.
- abecedarius 8y ago
  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. (Just trying to help; I like the idea.)
  - godelski 8y ago
    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.
alew1 8y ago
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.
Gehinnn 8y ago
Some time ago, I've implemented a non visual version of the incredible proof machine: http://hediet.de/projects/predicate-logic-proof-validator/examples/index.html?template=peano http://hediet.de/projects/predicate-logic-proof-validator/ex... Using the deduction theorem solver, you can easily generate solutions for some problems of the incredible proof machine.
thaumasiotes 8y ago
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.
- uryga 8y ago
  i was confused by the "local hypothesis" block as well until i realized it's just `lambda x: ...` :)
  - rogpeppe1 8y ago
    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. Any hints here?
    - rogpeppe1 8y ago
      OK, replying to myself for future reference. I found the answer here: https://youtu.be/0GeJdTTzaDo 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.
teddyh 8y ago
See also: Domino On Acid - Natural Deduction Visualized As A Game Of Dominoes http://www.winterdrache.de/freeware/domino/ http://www.winterdrache.de/freeware/domino/
scscsc 8y ago
I've worked on a similar project (https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html 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).
TheNewAndy 8y ago
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. https://screenshots.firefox.com/uhqTk89wKMgvig3n/books.google.com.au https://screenshots.firefox.com/uhqTk89wKMgvig3n/books.googl...
- catern 8y ago
  Isn't that the format that this site uses, at least on the task selection page? What do you mean?
popotamonga 8y ago
What did they use for the UI? I could use that block and connectors.
tempodox 8y ago
Wow, a web app that does something useful and doesn't have a host of bleeping social-media buttons. What a rare gem these days.

79 points by chewxy 8y ago

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.

abecedarius 8y ago
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. (Just trying to help; I like the idea.)
- godelski 8y ago
  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.

alew1 8y ago

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.

Gehinnn 8y ago

Some time ago, I've implemented a non visual version of the incredible proof machine: http://hediet.de/projects/predicate-logic-proof-validator/examples/index.html?template=peano http://hediet.de/projects/predicate-logic-proof-validator/ex... Using the deduction theorem solver, you can easily generate solutions for some problems of the incredible proof machine.

thaumasiotes 8y ago

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.

uryga 8y ago
i was confused by the "local hypothesis" block as well until i realized it's just `lambda x: ...` :)
- rogpeppe1 8y ago
  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. Any hints here?
  - rogpeppe1 8y ago
    OK, replying to myself for future reference. I found the answer here: https://youtu.be/0GeJdTTzaDo 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.

teddyh 8y ago

See also: Domino On Acid - Natural Deduction Visualized As A Game Of Dominoes http://www.winterdrache.de/freeware/domino/ http://www.winterdrache.de/freeware/domino/

scscsc 8y ago

I've worked on a similar project (https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html 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).

TheNewAndy 8y ago

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. https://screenshots.firefox.com/uhqTk89wKMgvig3n/books.google.com.au https://screenshots.firefox.com/uhqTk89wKMgvig3n/books.googl...

catern 8y ago
Isn't that the format that this site uses, at least on the task selection page? What do you mean?

popotamonga 8y ago

What did they use for the UI? I could use that block and connectors.

tempodox 8y ago

Wow, a web app that does something useful and doesn't have a host of bleeping social-media buttons. What a rare gem these days.