A, B, ..., Z | formulas |

, | to separate formulas |

( and ) | around a sub-formula |

|- or ⊢ | thesis sign |

Example: A0,A1,A2,B |- A',A''

^ | dual (e.g. A^) |

* or ⊗ | tensor (multiplicative conjunction) |

| or ⅋ | par (multiplicative disjunction) |

& | with (additive conjunction) |

+ or ⊕ | plus (additive disjunction) |

1 | one (multiplicative conjunction unit) |

bot or ⊥ or _ | bottom (multiplicative disjunction unit) |

top or ⊤ or T | top (additive conjunction unit) |

0 | zero (additive disjunction unit) |

-o or ⊸ | lollipop (linear implication) |

! | "of course" |

? | "why not" |

Example: !(A&B) |- !A*!B

- Exchange: you can drag and drop formulas to move them inside a sequent
- Axiom: click on the turnstile symbol or on an atomic formula
- Connectives: click to apply the introduction rule (if it is unique)
- Tensor: the context is split according to which formulas are on the left or on the right of the clicked tensor formula
- Plus: click on the sub-formula you want to keep for plus rules
- Why-not rules:
- single click on "?": weakening rule
- double click on "?": contraction rule
- single click on the sub-formula: dereliction rule

- If you change your mind, you can click again lower in the ongoing proof, or click on the rule name you want to undo.

- Non-provability checks: a red turnstile ⊢ means that the sequent is known not to be provable, however a black turnstile is not claiming anything about provability.
- "Auto-reverse": when switched on this option applies systematically reversible rules to generated sequents.
This includes not only the introduction rules for &, &, ⊥, ⊤, ! and 1, but also:
- axiom rule for atomic formulas
- dereliction rule on ?? formulas
- ⊗ rule with empty context

- Automated prover: you can double-click on a turnstile ⊢ to launch the auto-prover on a sequent. Three possibilities:
- the prover makes it, the proof is automatically filled up;
- the prover fails after an exhaustive research, the non-provable sequent is marked accordingly (red turnstile ⊢);
- the prover is stopped by time-out, it can not conclude on the provability of the sequent (orange turnstile ⊢).

- To export your proof in Coq format, click on button, even if it's still open proof. The file is self-documented.
- To export your proof in LaTeX format, click on button.
- To get your proof as LaTeX directly converted in PDF format, click on button.
- To get a screenshot of your proof as LaTeX in PNG format, click on button.

- Want to learn how to use this tool step by step? Try our tutorial.
- Not familiar with linear logic? Check the derivation rules.