C1ick & c⊗LLec⊥

Interactive linear logic prover

Syntax

Sequent syntax

A, B, ..., Z	formulas
,	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)
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

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.

⨯

Tutorial

Here is a short tutorial to learn how to interact with the tool. You should be able to have all example proofs complete (with green background).

Click on a formula or its orthogonal to apply the axiom rule.

{"s":{"cons":[{"t":"litt","v":"A"},{"t":"dual","v":{"t":"litt","v":"A"}}]},"ar":null}

If the two formulas are not explicitly orthogonal, you can click on thesis symbol to attempt to apply the axiom rule on a two-formulas sequent.

{"s":{"cons":[{"t":"one"},{"t":"bottom"}]},"ar":null}

Click on connectives to apply the associated rules.

{"s":{"cons":[{"t":"par","v1":{"t":"litt","v":"A"},"v2":{"t":"dual","v":{"t":"litt","v":"A"}}}]},"ar":null}

Move formulas within the list before applying tensor rule. Formulas on the left of the tensor formula will move to the left premise, and formulas on the right of the tensor formula will move to the right premise.

{"s":{"cons":[{"t":"litt","v":"A"},{"t":"dual","v":{"t":"litt","v":"A"}},{"t":"tensor","v1":{"t":"litt","v":"A"},"v2":{"t":"dual","v":{"t":"litt","v":"A"}}}]},"ar":null}

As for plus rules, just click on the left or right sub-formula.

{"s":{"cons":[{"t":"litt","v":"A"},{"t":"plus","v1":{"t":"litt","v":"B"},"v2":{"t":"dual","v":{"t":"litt","v":"A"}}}]},"ar":null}

For the whynot connective, you have three possibilities:

single click on whynot connective applies weakening
single click on the sub-formula applies dereliction
double click applies contraction.

{"s":{"cons":[{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"whynot","v":{"t":"litt","v":"B"}},{"t":"tensor","v1":{"t":"dual","v":{"t":"litt","v":"A"}},"v2":{"t":"dual","v":{"t":"litt","v":"A"}}}]},"ar":null}

That's it! Here are some extra examples for you to prove. Have fun!

You can play with yet another list of examples if you want.

⨯

Derivation rules

{"s":{"cons":[{"t":"litt","v":"A"},{"t":"dual","v":{"t":"litt","v":"A"}}]},"ar":{"rr":{"r":"axiom"},"p":[]}}

{"s":{"cons":[{"t":"one"}]},"ar":{"rr":{"r":"one"},"p":[]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"bottom"},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"bottom","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"Δ"}]},"ar":null}]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"top"},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"top","fp":1},"p":[]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"tensor","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"tensor","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"}]},"ar":null},{"s":{"cons":[{"t":"litt","v":"B"},{"t":"litt","v":"Δ"}]},"ar":null}]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"par","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"par","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"},{"t":"litt","v":"B"},{"t":"litt","v":"Δ"}]},"ar":null}]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"with","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"with","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"},{"t":"litt","v":"Δ"}]},"ar":null},{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"B"},{"t":"litt","v":"Δ"}]},"ar":null}]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"plus","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"plus_left","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"},{"t":"litt","v":"Δ"}]},"ar":null}]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"plus","v1":{"t":"litt","v":"A"},"v2":{"t":"litt","v":"B"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"plus_right","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"B"},{"t":"litt","v":"Δ"}]},"ar":null}]}}

{"s":{"cons":[{"t":"whynot","v":{"t":"litt","v":"Γ"}},{"t":"ofcourse","v":{"t":"litt","v":"A"}},{"t":"whynot","v":{"t":"litt","v":"Δ"}}]},"ar":{"rr":{"r":"promotion","fp":1},"p":[{"s":{"cons":[{"t":"whynot","v":{"t":"litt","v":"Γ"}},{"t":"litt","v":"A"},{"t":"whynot","v":{"t":"litt","v":"Δ"}}]},"ar":null}]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"weakening","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"Δ"}]},"ar":null}]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"dereliction","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"},{"t":"litt","v":"Δ"}]},"ar":null}]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"contraction","fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"whynot","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":null}]}}

{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"cut","formula":{"t":"litt","v":"A"},"fp":1},"p":[{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"litt","v":"A"}]},"ar":null},{"s":{"cons":[{"t":"dual","v":{"t":"litt","v":"A"}},{"t":"litt","v":"Δ"}]},"ar":null}]}}

	Tex	LaTeX code
	PDF	LaTeX converted in PDF format
	PNG	LaTeX converted in PNG format
	ASCII	Text representation using ASCII characters only
	UTF-8	Text representation using UTF-8 characters (better displayed with fixed width fonts)