[Provability checks] Empty sequent may be provable with cuts and cyclic notations

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

[Provability checks] Empty sequent may be provable with cuts and cyclic notations #139

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

The provability check make the turnstile red in: https://click-and-collect.linear-logic.org/?s=&n=a%2C%3Fa%5E While there is a proof.

etiennecallies commented 3 years ago

Good catch! So "because" of cut, if there is any cyclic notation (even not used in current sequent), we just can't determine provability of given sequent. Right?

olaure01 commented 3 years ago

Indeed, there is probably nothing safe to say regarding provability checks with both cuts and cyclic notations.