Home

Roadmap

• Coq/Yalla export
• LaTeX export
• add cut rule (issue #12)

Examples

• A⊗B ⊢ B⊗A
• (A⊗B)⊗C ⊢ A⊗(B⊗C)
• A⊗(B⊸C) ⊢ B⊸(A⊗C)
• A⊗(B⊕C) ⊢ (A⊗B)⊕(A⊗C)
• !(A&B) ⊢ !A⊗!B
• !A⊗!B ⊢ !(A&B)
• A⊗(A⊸A) ⊢ A⊗!(A⊸A)
• ((A⊸R)⊸R)⊗((B⊸R)⊸R) ⊢ ((A⊗B)⊸R)⊸R
• ((A⊸R)⊸R)⊕((B⊸R)⊸R) ⊢ ((A⊕B)⊸R)⊸R
• ((A⊸?B)⊸A)⊸?A
• !(A⅋B)⊸(?!?A⅋?!?B)
• ((((0⊸1)⊸1)⊸0)⊸0)⊸1
• (((X⊗⊤)&(Y⊗⊤))⊸0)⊸((X⊸X')⊕(Y⊸Y'))