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

Apply reversible first #158

Closed etiennecallies closed 3 years ago

etiennecallies commented 3 years ago

Specs:

click on a reversible connective (including ! in ?-context): applies the corresponding rule and do the corresponding reversing in the above proof (may require some axiom expansion steps, and modifying hypotheses as well)

Can not apply on preprod now, due to maintenance.

olaure01 commented 3 years ago

When clicking on a & connective in the conclusion of a & rule with twice the same premise, a strange proof-copying is involved. Try clicking on the lower & connective in this proof.

etiennecallies commented 3 years ago

When clicking on a & connective in the conclusion of a & rule with twice the same premise, a strange proof-copying is involved. Try clicking on the lower & connective in this proof.

Good catch 👍🏻

olaure01 commented 3 years ago

Double click reverses hereditarily the reversible sub-formulas? Dedicated button for full reversing of all concluding reversible formulas (including reversible sub-formulas)?

olaure01 commented 3 years ago

Trying to reverse a ! with not a ?-context generates an error message Can not apply 'promotion' rule: the context must contain formulas starting by '?' only. It is OK, but just to mention that an alternative would be not to activate reversibility of ! in such a situation. Not sure what is the best to do.

etiennecallies commented 3 years ago

I opened #163 for the enhancements of this feature.