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

Remove loop up to exchange and up to weakening #110

Closed etiennecallies closed 3 years ago

etiennecallies commented 3 years ago

Related issue: https://github.com/etiennecallies/click-and-collect/issues/94

Once preprod is free, I'll deploy it.

?(A*A),?((?1*_)+?(A*A)),?(A^|A^),??1 Before: ccLLproof (10) After: ccLLproof (12)

A^,A^, ?((?1⊗⊥)⊕??(A⊗A)),???(A*A) Before: ccLLproof (13) After: ccLLproof (14)

etiennecallies commented 3 years ago

?!?!(X|X^), ?!?!?!(Y|Y^) no more loop up to weakening https://linearon.modusponens.dev/?s=%3F%21%3F%21%28X%7CX%5E%29%2C+%3F%21%3F%21%3F%21%28Y%7CY%5E%29

olaure01 commented 3 years ago

Fixes #94

etiennecallies commented 3 years ago

@olaure01 it seems not trivial to compare proof from one branch to the other. Do you see an example where it would be make the proof simpler?