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
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.
Some of the examples here were implemented for the following papers:
A formal framework for specifying sequent calculus proof systems [pdf] by Dale Miller and Elaine Pimentel,
submitted to Theoretical Computer Science (TCS), 2012.
On the Complexity of Linear Authorization Logics [pdf] by Vivek Nigam, to appear in Logic
in Computer Science (LICS), 2012