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
19 stars 2 forks source link

Auto reverse #58

Closed etiennecallies closed 3 years ago

etiennecallies commented 3 years ago

Deployed on https://linearon.modusponens.dev/

etiennecallies commented 3 years ago

Integrates #51 even if it doesn't reuse code.

olaure01 commented 3 years ago

Could be natural to reverse all current open premises when mode is activated. Otherwise one need to click at least once to launch it, for example on the starting sequent if one wants to start reversing from the beginning.

olaure01 commented 3 years ago

No red turnstile on intermediary sequents. Are checks applied? Or they could be inferred downwards a posteriori: a reversible rule with a non provable premise has a non provable conclusion.

etiennecallies commented 3 years ago

Could be natural to reverse all current open premises when mode is activated. Otherwise one need to click at least once to launch it, for example on the starting sequent if one wants to start reversing from the beginning.

I agree, I'll do it on another PR.

etiennecallies commented 3 years ago

No red turnstile on intermediary sequents. Are checks applied?

I agree the checks should be called on intermediary sequent. I'll do that on another PR.

Or they could be inferred downwards a posteriori: a reversible rule with a non provable premise has a non provable conclusion.

Nice trick :) I'll see how I do that.