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

Proof nets #174

Open suhr opened 1 year ago

suhr commented 1 year ago

Sequents are nice, but proof nets would be even better.

olaure01 commented 1 year ago

Can you tell a bit more about what you would like? interactive building of proof nets ? export into proof nets ? It is not a simple matter in general as even drawing a proof net from a sequent calculus proof is not immediate if you want a nice output.

suhr commented 1 year ago

Interactive building and cut elimination.

It is not a simple matter in general as even drawing a proof net from a sequent calculus proof is not immediate if you want a nice output.

If you don't try to transform a sequent proof, but want to just represent a graph as a text, then it's easy to do with variables. Something like

WIRES m1:M, m2:M, n1:N1, n2:N2;

c(m1,m2,m) cut(m,t1) ⊕(t1,b1,t2)
!(b1) { … }
⊕(t2, b2, a)
!(b2, n2) { … }
ax(a, n1)

You only need to ensure that variable names are unique and that the types match + usual checks for a proof structure being a proof net. Though the later might be hard to check for a usual (not polarized) proof net.