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 on open proofs may change the order of formulas in open leaves #172
Open
olaure01 opened 2 years ago
The left open leaf is modified by (one-step) reducing the cut in this proof. And the next step generates a
Technical error.