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 cyclic notations #131

Closed etiennecallies closed 3 years ago

etiennecallies commented 3 years ago

Fixes #128

etiennecallies commented 3 years ago

Works on preprod https://linearon.modusponens.dev/?s=o&n=o%2Co-oo The returned proof is not always the simplest one we could think of https://linearon.modusponens.dev/?s=%3FA&n=A%2C%3FB%2B%3FC&n=B%2CA&n=C%2CA%5E but at least it works