A cute tatu.

Online system for reasoning about sequent calculus specifications in linear logic with subexponentials
Developed by: Giselle Reis and Vivek Nigam
Contact: giselle [at] logic [dot] at
Based on the theoretical work: An Extended Framework for Specifying and Reasoning about Proof Systems [pdf | slides]- Vivek Nigam, Elaine Pimentel and Giselle Reis

What property would you like to check?

Transformation to principal cut

Check if the rules permute in such a way that is possible to obtain principal cuts.


Check if principal cuts can be simplified using the rewritting rules of cut-elimination until there are only cuts on atoms.

Elimination of atomic cuts

Check if the atomic cuts can be eliminated.


Check if the proof systems is complete using only atomic axioms.

You can type your own system or try one of our examples:

PS: You can drag this window around and keep it open for a quick reference.

Some of the examples here were implemented for the following papers: