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.

Cut-coherence

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.

Initial-coherence

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: