search

nomeata / incredible

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

Scope calculation in partial graphs too generous #91

Closed sjakobi closed 2 years ago

sjakobi commented 7 years ago

I believe this proof is correct but the IPM rejects it:

bildschirmfoto_2017-01-12_11-18-57

nomeata commented 7 years ago

Well, the proposition ∀x.P(c) (for some constant c, here called y3) is different from the proposition ∀x.P(x). And why is the c constant? Because your ∀-introduction block requires you to prove P(x) for any x, but you provide it for a fixed y3. So the P of the ∀-intro-block gets unified with x ↦ P(y3), i.e. a constant proposition not using x at all.

You are fighting some of the intricacies of quantifiers, local constants and their scope, which are insufficiently well visualized.

sjakobi commented 7 years ago

Thanks for the explanation! I think I understand what you say but I haven't solved the problem yet.

Regarding the visualisation, what surprised me, was that in this incomplete state, the ∀-intro-block seems to work as I wanted it to work:

bildschirmfoto_2017-01-13_08-51-15

Shouldn't the IPM already be able to tell me that P(c5) can't be generalised to ∀x.P(x)?

nomeata commented 7 years ago

Hmm, interesting. I would have indeed expected c5 to be invalid at block 3, as block 3 is not in the scope of 5’s input (in the terminology of http://pp.ipd.kit.edu/uploads/publikationen/breitner16incredible.pdf). But with partial graphs, the calculation of the scopes is a bit more tricky. We can leave this issue to track that.

ChristopherKing42 commented 6 years ago

Same bug here

screenshot 2017-12-01 at 8 20 26 pm

It should show P(c_4) where it show P(y_6). Using the annotation block doesn't help either.

nomeata commented 6 years ago

Not sure if this example is a bug: The scope y6 is everywhere to the left of the ∃ block. The scope of c4 is everywhere left of the ∀ block. Unification would require y6=c4, but then c4 would appear to the right of the ∀ block, which is not allowed. Therefore, this unification fails.

nomeata commented 2 years ago

I believe there is no actual bug here, so closing. Please reopen if I am mistaken.