commute weakenings downwards

[etiennecallies]

• I removed the remove_loop since it seems that commuting weakenings is enough to prevent looping in proof result. I would be happy to set it back if we find a counter-example.
• I didn't succeed in finding an example where weakenings above With are not in the same order in both premises. If we find an example then we'll have to handle this case.

[olaure01]

* I removed the `remove_loop` since it seems that commuting weakenings is enough to prevent looping in proof result. I would be happy to set it back if we find a counter-example.

What about issue #84 ?

[etiennecallies]

* I removed the `remove_loop` since it seems that commuting weakenings is enough to prevent looping in proof result. I would be happy to set it back if we find a counter-example.

What about issue #84 ?

Well, I can't reproduce the issue on https://linearon.modusponens.dev/?s=%21%28%3F%21A%261%29+%E2%8A%A2+%3F%21A

[olaure01]

Probably nothing to do with weakening but because of the new call loop for the prover which explores "short" proofs first in pre-prod. I do not remember exactly which version is in prod but possibly the one working directly with bound 3.

[olaure01]

I didn't succeed in finding an example where weakenings above With are not in the same order in both premises.

There is at least this: 1,?(A*A),?(B*B*B)&?C. I am still trying to figure out if it can be worse with the current prover.

[etiennecallies]

Probably nothing to do with weakening but because of the new call loop for the prover which explores "short" proofs first in pre-prod. I do not remember exactly which version is in prod but possibly the one working directly with bound 3.

You're absolutely right! I Nothing to do with weakenings. I tried with fixed exponential bound to 3, and there is a loop. Do we assume that the way we increment exponential bound prevents from looping? Or do I put back the remove_loop method?

[olaure01]

Here is a loop: ?_,??(1&1). But I don't know if it occurs before weakening commutation.

[etiennecallies]

I didn't succeed in finding an example where weakenings above With are not in the same order in both premises.

There is at least this: 1,?(A*A),?(B*B*B)&?C. I am still trying to figure out if it can be worse with the current prover.

I just added a commit with a swap on weakenings above With, and this solve this particular case https://linearon.modusponens.dev/?s=1%2C%3F%28A*A%29%2C%3F%28B*B*B%29%26%3FC

But doesn't solve this one https://linearon.modusponens.dev/?s=%3FA%5E%2C%28A%7CA%29%261%2C%3F%28B*B%29%2C%3F%28_*_%29

[olaure01]

Yep. Similar examples: ??1,?(_&1) or ?1,?A,_&1

[etiennecallies]

?_,??(1&1)

Fair enough :) I put the remove_loop method back.

[olaure01]

Look at: (1|1)*_,?(?1*?1) Loop generated after weakening commutation on the left, and stupid proof on the right (but this is what the algorithm is asked to do: select big ?-formulas first). So loop-detection should be run again after weakening commutation. I don't know if it is better to put it before exchange-commutation or after or both.

[etiennecallies]

Look at: (1|1)*_,?(?1*?1) Loop generated after weakening commutation on the left, and stupid proof on the right (but this is what the algorithm is asked to do: select big ?-formulas first). So loop-detection should be run again after weakening commutation. I don't know if it is better to put it before exchange-commutation or after or both.

Before exchange commutations:

After exchange commutations:

Both:

I vote both.

[olaure01]

Concerning the additive/weakening commutation, another example similar to those above:

!(?!A&?!B) ⊢ !?(!A&!B)

but probably interesting to add it to the test suite as well since it is in the list of examples.

[etiennecallies]

Concerning the additive/weakening commutation, another example similar to those above:

!(?!A&?!B) ⊢ !?(!A&!B)

but probably interesting to add it to the test suite as well since it is in the list of examples.

I added a test that checks that the simplified proof is exactly this one https://linearon.modusponens.dev/?s=%21%28%3F%21A%26%3F%21B%29+%E2%8A%A2+%21%3F%28%21A%26%21B%29