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

Propagate non-provability through reversible rules #83

Closed etiennecallies closed 3 years ago

etiennecallies commented 3 years ago

When the auto-prover returns non-provable, all conclusions of reversible rules should be marked as non-provable.

Requires: save the reversible information.

olaure01 commented 3 years ago

This possibly applies to non-provability checks as well. Doing more than just going down ⅋, &, ⊥, ! is probably meaningless (at least to start): others like context-free tensor rule are quite specific.

etiennecallies commented 3 years ago

Ok then it would be not too hard to do it on javascript side.