C1ick & c⊗LLec⊥

Interactive linear logic prover

Syntax

Sequent syntax

A, B, ..., Zformulas
,to separate formulas
( and )around a sub-formula
|- or thesis sign

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

Linear logic formulas

^dual (e.g. A^)
* or tensor (multiplicative conjunction)
| or par (multiplicative disjunction)
&with (additive conjunction)
+ or plus (additive disjunction)
1one (multiplicative conjunction unit)
bot or or _bottom (multiplicative disjunction unit)
top or or Ttop (additive conjunction unit)
0zero (additive disjunction unit)
-o or lollipop (linear implication)
!"of course"
?"why not"

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

Help

Interactions

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

Assisted-proving features

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

Export

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

Tutorial

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

When switched-on this option applies systematically reversible rules to generated sequents.
This includes not only the introduction rules for &, &, ⊥, ⊤, ! and 1, but also:

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:

Next to cut rules:

Inside sequents:

Some global action buttons will also appear below proof:

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.