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

Cut-coherence

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

Check

Elimination of atomic cuts

Check if the atomic cuts can be eliminated.

Check

Initial-coherence

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

Check

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

Help Reset

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

⊗ → *
⊕ → +
& → &
⅋ → |
!^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

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 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.

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