Home - ComputerAidedLL/click-and-collect GitHub Wiki
- extending special mode for proof transformations: reversing, focusing, etc.
- add colors to follow occurrences
- two-sided sequent calculus
- intuitionistic linear logic (click on a comma to apply right-hand side ⊗-rule)
- other linear logic variants (ELL, SLL, LLL, etc.)
- quantifiers (issue #16)
- 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)
- explicit exchange rule (with colored backgrounds to follow instances of formulas) (issue #11)
- back edges for regular proofs
- fixed-point connectives in formulas
- mix rules (note mix2 can be faithfully simulated by adding
?(⊥⊗⊥)in the context, and similarly for mix0 with?1) - export to proof-nets