search

nomeata / incredible

The Incredible Proof Machine
MIT License
358 stars 36 forks source link

Please explain these complicated blocks #115

Closed void4 closed 5 years ago

void4 commented 5 years ago

I've searched far and wide, but I couldn't find a single introduction to what these blocks represent and how they behave.

It seems that this implication block gives you the left side as an assumption which you can then use to prove (possibly in combination with other assumptions) the right hand side. After that, you get the full implication. It seems that the assumption can only be used to feed back into the right side. Is this correct? image

The following is essentially black magic to me, I don't know at all how it behaves. From this video it seems that you when you want to prove the output, you have to prove it for both sides of the input separately. image

nomeata commented 5 years ago

Did you also look at http://pp.ipd.kit.edu/uploads/publikationen/breitner16incredible.pdf ?

nomeata commented 5 years ago

It seems that the assumption can only be used to feed back into the right side. Is this correct?

Correct

when you want to prove the output, you have to prove it for both sides of the input separately.

Correct

Looks like you understand them after all :-)

void4 commented 5 years ago

The pdf seems to be what I've been looking for, thank you for your responses. It would be great to incorporate that into some tutorial directly on the site, which would make it easier to find.

It isn't really clear to me yet why one gets these assumptions (X,Y) "for free" and what exactly the scoping rules are, so I'll leave this issue open for now and come back later.

nomeata commented 5 years ago

Yeah, a good tutorial would be good, but beyond what I can invest into the program at the moment, unfortunately.