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-prover with non-recursive notations #127

Closed etiennecallies closed 3 years ago

etiennecallies commented 3 years ago

Works on preprod: https://linearon.modusponens.dev/?s=A&n=A%2CB%7CB&n=B%2C%3F1

etiennecallies commented 3 years ago

Maybe update help about orange ⊢.

I precised recursive in Help. You can suggest an edit if you see of a better way to say it.

etiennecallies commented 3 years ago

I was wondering whether it could be interesting to consider the following approach to cyclic notations: spend 2s searching for a proof without using these cyclic notations at all (just like now), spend 0.5s after a single round of unfolding of each of them, spend 0.5s for a depth 2 unfolding, then fail.

https://github.com/etiennecallies/click-and-collect/issues/128

olaure01 commented 3 years ago

Maybe update help about orange ⊢.

I precised recursive in Help. You can suggest an edit if you see of a better way to say it.

I missed it, sorry. Perfect.