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

Export

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

Tutorial

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