Home

Roadmap

Ongoing work

• Coq/Yalla export
• LaTeX and image export
• user call to an automated prover (this includes some proof import)
• add cut rule (issue #12)
• explicit exchange rule (with colored backgrounds to follow instances of formulas) (issue #11)
• formula naming through (possibly recursive) equations (with click on name to unfold a definition inside a proof)

  𝔹 ::= (A ⊗ A) ⊸ (A ⊗ A)
  ℕ ::= !(A ⊸ A) ⊸ !(A ⊸ A)
  o ::= !o ⊸ o
  

Other directions

• two-sided sequent calculus
• intuitionistic linear logic
• quantifiers (issue #16)
• auto-reverse mode: automatically apply reversible rules
• automatic detection of non-provable sequents (by call to sufficient conditions and to an automated prover)
• contexts as first-class objects (issue #13)
• cyclic linear logic (exchange restricted to circular shifts, requires to modify the definition of dual of a formula)
• additional tool for proof transformations (cut elimination, axiom expansion, reversing, focusing, substitution, etc.) (issue #12)
• back edges for regular proofs
• fixed-point connectives in formulas
• mix rules (note mix₂ can be faithfully simulated by adding ?(⊥⊗⊥) in the context, and similarly for mix₀ with ?1)
• export to proof-nets

Examples

1. A⊗B ⊢ B⊗A
2. (A⊗B)⊗C ⊢ A⊗(B⊗C)
3. A⊗(B⊸C) ⊢ B⊸(A⊗C)
4. A⊗(B⊕C) ⊢ (A⊗B)⊕(A⊗C)
5. !(A&B) ⊢ !A⊗!B
6. !A⊗!B ⊢ !(A&B)
7. !A⊗!B ⊢ !(A⊗B)
8. A⊗(A⊸A) ⊢ A⊗!(A⊸A)
9. !(!A⊸B), !(!B⊸C) ⊢ !A⊸C
10. A⊗A⊸A⊗A
11. !(A⊸A)⊸!(A⊸A)
12. ((A⊸R)⊸R)⊗((B⊸R)⊸R) ⊢ ((A⊗B)⊸R)⊸R
13. ((A⊸R)⊸R)⊕((B⊸R)⊸R) ⊢ ((A⊕B)⊸R)⊸R
14. ((A⊸?B)⊸A)⊸?A
15. !(A⅋B)⊸(?!?A⅋?!?B)
16. ⊢ ?A, ?(B⅋B), ?(A^⊥⅋B^⊥), ?(⊥⊗⊥)
17. ((((0⊸1)⊸1)⊸0)⊸0)⊸1
18. (((A⊗⊤)&(B⊗⊤))⊸0)⊸((A⊸A')⊕(B⊸B'))