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

[auto-prove] No proof found while OK with Wu's prover #90

Closed olaure01 closed 3 years ago

olaure01 commented 3 years ago

Automated prover stops with no proof found after 3s while Wu's prover is answering immediately:

⊢ X^⊗X^, X, ?(X^⊗(X⅋X))
olaure01 commented 3 years ago

It might be that after a bad context split in a tensor rule, a non-provable sequent (here ⊢ X^, ?(X^⊗(X⅋X))) is addressed in which an infinite sequence of calls to apply_d2 is run by scanning all possible max_d2 (-1, -2, etc.).

etiennecallies commented 3 years ago

Oh yes, it might be that, let me see...