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.

I want to check whether the rule
permutes over the rule

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