| CARVIEW |
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.
- 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.
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.
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.
Click on connectives to apply the associated rules.
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.
As for plus rules, just click on the left or right sub-formula.
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.
That's it! Here are some extra examples for you to prove. Have fun!
- A⊗B ⊢ B⊗A
- (A⊗B)⊗C ⊢ A⊗(B⊗C)
- A⊗(B⊸C) ⊢ B⊸(A⊗C)
- A⊗(B⊕C) ⊢ (A⊗B)⊕(A⊗C)
- !A⊗!B ⊢ !(A⊗B)
- !(A&B) ⊢ !A⊗!B
- !A⊗!B ⊢ !(A&B)
You can play with yet another list of examples if you want.
Derivation rules
This tool design was mainly inspired by Logitext.