search

ComputerAidedLL / click-and-collect

A web interactive tool for building proofs in the sequent calculus of Linear Logic, with its backend written in OCaml
GNU Lesser General Public License v2.1
17 stars 2 forks source link

[auto-reverse] dereliction on ??-formulas is not canonical #95

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

The two proofs of ⊢ ??0, 1 using weakening directly or first dereliction and then weakening are different (not the same relational semantics for example). This means dereliction on ??-formulas should not be applied in auto-reverse mode since we want all those operations not to impact the possible semantics of the obtained proofs.

One could however integrate this as an optimization in the automated prover: before moving a ?-formula to the exponential part of focused sequents, remove n-1 ?-connectives if it starts with n ?-connectives.

olaure01 commented 3 years ago

Sorry, this is entirely my fault. Concerning the automated prover, I am not sure this is the right place here to work on optimizing it.

etiennecallies commented 3 years ago

Regarding the auto-prover and the "remove (n-1) ?" trick, it may break the "focus" structure, but there must be an easy way to do it. I let you open a new discussion, if you think it's worth it.

olaure01 commented 3 years ago

I would extend the focused system with a rule of the shape:

⊢ Δ | Γ ⇑ ?A, Λ
----------------
⊢ Δ | Γ ⇑ ??A, Λ

to be applied before the more general one with conclusion ⊢ Δ | Γ ⇑ ?A, Λ. But it do not think it should be a priority here.