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.
- 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 generate a drawing of your proof click on button. You will then be able to select among: LaTeX source, PDF export, PNG image, Ascii or UTF8 representation.
- To get an url link to your proof to share or reuse it, 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.

- Click on + button to add a new notation.
- Click on an existing notation to edit or delete it.
- Recursive notations are allowed.

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
- ⊗ rule with empty context

When switched-on this option allows you to apply cut rule. Click on the position you would like to cut (a comma , between two formulas or a point . at the beginning or end of a sequent), and type your formula in the popup.

When switched-on this option allows you to work on a proof. You may see some action buttons (enabled or not) appear next to rule names.

Next to axioms:

- Click on ⇫ button to expand an axiom rule (applies reversible rules first).
- Click on ⇯ button to fully expand an axiom rule (disabled on proof with recursive notations).

Next to cut rules:

- Click on ← (resp. →) button to commute a cut rule on left (resp. right) hand-side.
- Click on ↑ to eliminate a cut rule on key-case.
- Click on ✄ to eliminate a specific cut completely (disabled on proof with recursive notations).

Inside sequents:

- Click on reversible connectives (&, &, ⊥, ⊤, !) to apply them first.

Some global action buttons will also appear below proof:

- Click on ↶ (resp. ↷) button below proof to undo (resp. redo) last transformation.
- Click on ↯ button below proof to simplify proof (commute up exchanges, commute down weakenings).
- Click on ✄ button below proof to eliminate all cuts in the proof (disabled on proof with recursive notations).

By default, no exchange rule will appear in the export: the output will be displayed as in the interface (snapshot). With explicit exchange activated, required exchanges will appear in the export, to get derivation rules applied strictly through the proof.