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

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.

Check if the atomic cuts can be eliminated.

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

- Type your specification in the text box indicated. Here is a quick syntax reference:

⊗ → *Note that ∞ is the maximal subexponential (it is greater than every other index) that holds the formulas of the specification. It is unbounded. The operators

⊕ → +

& → &

⅋ → |

!^{l}→ [l]bang

?^{l}→ [l]?

!^{∞}→ bang

?^{∞}→ ?

1 → one

0 → zero

⊤ → top

⊥ → bot

⌈A⌉ → rght A

⌊A⌋ → lft A

⌈A:x⌉ → mrght A X

⌊A:x⌋ → mlft A X

`bang`and`?`can be used to simulate the exponential operators of Linear Logic. - Type the signature in the text box indicated. You might want to use
the keywords
`form`and`term`for types of object level formulas and terms, respectively. - Lines beginning with
`%`are comments. - Choose what you want to check on the left and click check.

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