Online system for checking permutation of sequent calculus rules.
Developed by: Giselle Reis, Vivek Nigam and Leonardo Lima
Contact: giselle [at] logic [dot] at or leonardo [dot] alfs [at] gmail [dot] com
Based on the theoretical work: Checking Proof Transformations with ASP
[pdf|presentation]- Vivek Nigam, Giselle Reis and Leonardo Lima
This web-interface provides only limited functionality. The full system can be downloaded here.
Render the inference rules of the specified system.
The rules of the system are the following:
I want to check whether the rule
permutes over the rule
The bipoles of the system are the following:
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.