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

Fixed bound to 4. #91

Closed etiennecallies closed 3 years ago

etiennecallies commented 3 years ago

Fixes #90

I try several possibilities of bound, 4 is required to prove all proofs in test. 5 is slower, 6 is too slow for certain sequents.

We probably have to be smarter in the future.

What do you think @olaure01 ?

olaure01 commented 3 years ago

The alternative would be to have an external loop calling the prover with 0, 1, 2, 3, etc. until time-out is reached (or starting with bigger initial value than 0, but this might miss shorter proofs if I remember well).