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

Cut elimination, one at a time #119

Closed lionelvaux closed 3 years ago

lionelvaux commented 3 years ago

Salut,

Thanks to #108, we can now write proofs with cuts, which solves the first part of #12. Excellent job, thank you for that!

The second part remains: eliminating cuts, interactively. If click-and-collect is to be used as a pedagogical tool for teaching linear logic, I believe that this should be given a high priority among the list of possible enhancements.

Discussion about this in the thread for #12 led to the more general idea of implementing a separate tool/frontend for proof transformations. I am not sure this should be a completely separate tool, because it must share some of the data types and general design of the current implementation, but it is of course a major addition, and should correspond to a different mode (that would certainly be made accessible only after completing the proof, although some operations can be performed on open proofs). And starting with cut elimination seems like the way to go because:

  1. it is central to the theory of linear logic;
  2. it fits well with the general spirit of click-and-collect: interact with proof objects by clicking on the focus of the operation to be performed (here, the cut to be eliminated, rather than the formula to be introduced);
  3. please! :-)

I would be happy to discuss possible solutions or design choices, and contribute to the effort at least by testing and hunting bugs.

olaure01 commented 3 years ago

This feature is under consideration as an enhancement proposal.

etiennecallies commented 3 years ago

This feature is now in production.