We have formalized of semi-substructural logics with additive connectives.
The extension with addtive conjunction and disjunction is fully formalized, including
- cut-free sequent calculus,
- focused sequent calculus, and
- correctness of the focused caclculus.
The formalization uses Agda 2.6.3.