<?xml version="1.0" encoding="utf-8" ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
    <head>
        <link rel="canonical" href="https://click-and-collect.linear-logic.org/" />
        <script src="static/jquery/jquery-3.6.0.min.js" type="text/javascript"></script>
        <script src="static/jquery/jquery-ui.min.js" type="text/javascript"></script>
        <!-- JQuery on mobile -->
        <script type="text/javascript" src="static/jquery/jquery.ui.touch-punch.min.js"></script>
        <script type="text/javascript" src="static/js/sequent.js"></script>
        <script type="text/javascript" src="static/js/proof.js"></script>
        <script type="text/javascript" src="static/js/app.js"></script>
        <link rel="stylesheet" type="text/css" href="static/css/jquery-ui.min.css">
        <link rel="stylesheet" type="text/css" href="static/css/jquery-ui.structure.min.css">
        <link rel="stylesheet" type="text/css" href="static/css/jquery-ui.theme.min.css">
        <link href="static/css/style.css" rel="stylesheet" type="text/css">
        <title>C1ick ⅋ c⊗LLec⊥ - Interactive linear logic prover</title>
        <link rel="shortcut icon" type="image/jpg" href="static/images/favicon.ico"/>
        <meta name="description" content="An interactive tool to build proofs in the sequent calculus of Linear Logic">
        <meta name="keywords" content="click, collect, click-and-collect, linear, logic, LL, sequent, calculus, proof, prover, propositional, interactive, online, latex, coq, pdf">
        <meta name="viewport" content="width=device-width, initial-scale=1.0">

        <!-- Global site tag (gtag.js) - Google Analytics -->
        <script async src="https://www.googletagmanager.com/gtag/js?id=G-6M0JK9PWN1" type="text/javascript"></script>
        <script type="text/javascript">
            window.dataLayer = window.dataLayer || [];
            function gtag(){dataLayer.push(arguments);}
            gtag('js', new Date());

            gtag('config', 'G-6M0JK9PWN1');
        </script>
    </head>
    <body>
        <div class="section-wrapper">
            <div class="section">
                <h2>C1ick <span class="flip">&</span> c⊗LLec⊥</h2>
                <h1>Interactive linear logic prover</h1>
            </div>
            <div class="section">
                <form action="#" id="sequent-form">
                    <label>
                        <input type="text" name="sequentAsString" placeholder="Type sequent to prove..." size="24" />
                    </label>
                    <input type="submit" value="Prove" onclick="submitSequent(this)">
                </form>
            </div>
        </div>

        <div class="section-wrapper">
            <div class="section main-proof-section">
                <div id="main-proof-container" class="proof-container">

                </div>
            </div>
        </div>

        <div class="section-wrapper darker-gray">
            <div class="section syntax">
                <h3>Syntax</h3>
                <div class="subsection">
                    <h4>
                        Sequent syntax
                    </h4>
                    <table>
                        <tr><td><span class="code">A</span>, <span class="code">B</span>, ..., <span class="code">Z</span></td><td>formulas</td></tr>
                        <tr><td><span class="code">,</span></td><td>to separate formulas</td></tr>
                        <tr><td><span class="code">(</span> and <span class="code">)</span></td><td>around a sub-formula</td></tr>
                        <tr><td><span class="code">|-</span> or <span class="code">⊢</span></td><td>thesis sign</td></tr>
                    </table>
                    <p>
                        <span class="example">Example: </span><span class="code">A0,A1,A2,B |- A',A''</span>
                    </p>

                </div>
                <div class="subsection">
                    <h4>
                        Linear logic formulas
                    </h4>
                    <table>
                        <tr><td><span class="code">^</span></td><td>dual (e.g. <span class="code">A^</span>)</td></tr>
                        <tr><td><span class="code">*</span> or <span class="code">⊗</span></td><td>tensor (multiplicative conjunction)</td></tr>
                        <tr><td><span class="code">|</span> or <span class="code">⅋</span></td><td>par (multiplicative disjunction)</td></tr>
                        <tr><td><span class="code">&</span></td><td>with (additive conjunction)</td></tr>
                        <tr><td><span class="code">+</span> or <span class="code">⊕</span></td><td>plus (additive disjunction)</td></tr>
                        <tr><td><span class="code">1</span></td><td>one (multiplicative conjunction unit)</td></tr>
                        <tr><td><span class="code">bot</span> or <span class="code">⊥</span> or <span class="code">_</span></td><td>bottom (multiplicative disjunction unit)</td></tr>
                        <tr><td><span class="code">top</span> or <span class="code">⊤</span> or <span class="code">T</span></td><td>top (additive conjunction unit)</td></tr>
                        <tr><td><span class="code">0</span></td><td>zero (additive disjunction unit)</td></tr>
                        <tr><td><span class="code">-o</span> or <span class="code">⊸</span></td><td>lollipop (linear implication)</td></tr>
                        <tr><td><span class="code">!</span></td><td>"of course"</td></tr>
                        <tr><td><span class="code">?</span></td><td>"why not"</td></tr>
                    </table>
                    <p>
                        <span class="example">Example: </span><span class="code">!(A&B) |- !A*!B</span>
                    </p>
                </div>
            </div>
        </div>

        <div class="section-wrapper light-gray">
            <div class="section memo">
                <h3>Help</h3>
                <div class="subsection">
                    <h4>
                        Interactions
                    </h4>
                    <ul>
                        <li><span class="bold">Exchange:</span> you can drag and drop formulas to move them inside a sequent</li>
                        <li><span class="bold">Axiom:</span> click on the turnstile symbol or on an atomic formula</li>
                        <li><span class="bold">Connectives:</span> click to apply the introduction rule (if it is unique)</li>
                        <li><span class="bold">Tensor:</span> the context is split according to which formulas are on the left or on the right of the clicked tensor formula</li>
                        <li><span class="bold">Plus:</span> click on the sub-formula you want to keep for plus rules</li>
                        <li><span class="bold">Why-not</span> rules:
                            <ul>
                                <li>single click on "?": weakening rule</li>
                                <li>double click on "?": contraction rule</li>
                                <li>single click on the sub-formula: dereliction rule</li>
                            </ul>
                        </li>
                        <li>If you change your mind, you can click again lower in the ongoing proof, or click on the rule name you want to undo.</li>
                    </ul>
                </div>

                <div class="subsection">
                    <h4>
                        Assisted-proving features
                    </h4>
                    <ul>
                        <li><span class="bold">Non-provability checks:</span> a red turnstile <span class="turnstile not-provable">⊢</span> means that the sequent is known <span class="bold">not to be provable</span>, however a black turnstile is not claiming anything about provability.</li>
                        <li><span class="bold">Automated prover:</span> you can <span class="bold">double-click on a turnstile ⊢</span> to launch the auto-prover on a sequent. Three possibilities:
                        <ul>
                            <li>the prover makes it, the proof is automatically filled up;</li>
                            <li>the prover fails after an exhaustive research, the non-provable sequent is marked accordingly (red turnstile <span class="turnstile not-provable">⊢</span>);</li>
                            <li>the prover is stopped by time-out, it can not conclude on the provability of the sequent (orange turnstile <span class="turnstile not-auto-provable">⊢</span>).</li>
                        </ul>
                    </ul>
                </div>

                <div class="subsection">
                    <h4>
                        Export
                    </h4>
                    <ul>
                        <li>To export your proof in Coq format, click on <img src="static/images/coq.png" title="Export as Coq" style="height:1em;" /> button, even if it's still open proof. The file is self-documented.</li>
                        <li>To generate a drawing of your proof click on <img src="static/images/camera.png" title="Proof drawing" style="height: 1em;" /> button. You will then be able to select among: LaTeX source, PDF export, PNG image, Ascii or UTF8 representation.</li>
                        <li>To get an url link to your proof to share or reuse it, click on <img src="static/images/share-icon.png" title="Share proof URL" style="height: 1em;" /> button.</li>
                    </ul>
                </div>

                <div class="subsection">
                    <h4>
                        Tutorial
                    </h4>
                    <ul>
                        <li>Want to learn how to use this tool step by step? Try our <a href="#tutorial" onclick="showTutorial();">tutorial</a>.</li>
                        <li>Not familiar with linear logic? Check the <a href="#rules" onclick="showRules();">derivation rules</a>.</li>
                    </ul>
                </div>
            </div>
        </div>

        <div id="notations-dialog" title="Notations" class="dialog">
            <ul>
                <li>Click on + button to add a new notation.</li>
                <li>Click on an existing notation to edit or delete it.</li>
                <li>Recursive notations are allowed.</li>
            </ul>
        </div>

        <div id="auto-reverse-dialog" title="Auto-reverse option" class="dialog">
            <p>When switched-on this option applies systematically reversible rules to generated sequents.<br>
                This includes not only the introduction rules for <span class="flip">&</span>, &, ⊥, ⊤, ! and 1, but also:</p>
            <ul>
                <li>axiom rule for atomic formulas</li>
                <li>⊗ rule with empty context</li>
            </ul>
        </div>

        <div id="cut-mode-dialog" title="Cut mode option" class="dialog">
            <p>When switched-on this option allows you to apply cut rule.
                Click on the position you would like to cut (a comma <span class="code">,</span> between two formulas or a point <span class="code">.</span> at the beginning or end of a sequent), and type your formula in the popup.</p>
        </div>

        <div id="proof-transformation-dialog" title="Proof transformation mode" class="dialog">
            <p>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.</p>
            <p>Next to axioms:</p>
            <ul>
                <li>Click on ⇫ button to expand an axiom rule (applies reversible rules first).</li>
                <li>Click on ⇯ button to fully expand an axiom rule (disabled on proof with recursive notations).</li>
            </ul>
            <p>Next to cut rules:</p>
            <ul>
                <li>Click on ← (resp. →) button to commute a cut rule on left (resp. right) hand-side.</li>
                <li>Click on ↑ to eliminate a cut rule on key-case.</li>
                <li>Click on ✄ to eliminate a specific cut completely (disabled on proof with recursive notations).</li>
            </ul>
            <p>Inside sequents:</p>
            <ul>
                <li>Click on reversible connectives (<span class="flip">&</span>, &, ⊥, ⊤, !) to apply them first.</li>
            </ul>
            <p>Some global action buttons will also appear below proof:</p>
            <ul>
                <li>Click on ↶ (resp. ↷) button below proof to undo (resp. redo) last transformation.</li>
                <li>Click on ↯ button below proof to simplify proof (commute up exchanges, commute down weakenings).</li>
                <li>Click on ✄ button below proof to eliminate all cuts in the proof (disabled on proof with recursive notations).</li>
            </ul>
        </div>

        <div id="cut-formula-dialog" title="Enter cut formula" class="dialog">
            <form action="#">
                <label>
                    <input type="text" name="formulaAsString" placeholder="Type formula ..." size="26" />
                </label>
                <input type="submit" value="Cut" />
            </form>
        </div>

        <div id="substitution-formula-dialog" title="Enter substitution formula" class="dialog">
            <form action="#">
                <label>
                    <input type="text" name="alias" size="2" />
                    <span>≔</span>
                    <input type="text" name="formulaAsString" placeholder="Type formula ..." size="20" />
                </label>
                <input type="submit" value="Substitute" />
            </form>
        </div>

        <div id="explicit-exchange-dialog" title="Explicit exchange" class="dialog">
            <p>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.</p>
        </div>

        <div id="export-dialog" title="Choose export options" class="dialog">
            <table>
                <tr><td><input type="radio" id="tex" name="format" value="tex" checked></td>
                    <td><label for="tex"><span class="bold">Tex</span></label></td>
                    <td><label for="tex">LaTeX code</label></td></tr>
                <tr><td><input type="radio" id="pdf" name="format" value="pdf"></td>
                    <td><label for="pdf"><span class="bold">PDF</span></label></td>
                    <td><label for="pdf">LaTeX converted in PDF format</label></td></tr>
                <tr><td><input type="radio" id="png" name="format" value="png"></td>
                    <td><label for="png"><span class="bold">PNG</span></label></td>
                    <td><label for="png">LaTeX converted in PNG format</label></td></tr>
                <tr><td><input type="radio" id="ascii" name="format" value="ascii"></td>
                    <td><label for="ascii"><span class="bold">ASCII</span></label></td>
                    <td><label for="ascii">Text representation using ASCII characters only</label></td></tr>
                <tr><td><input type="radio" id="utf8" name="format" value="utf8"></td>
                    <td><label for="utf8"><span class="bold nowrap">UTF-8</span></label></td>
                    <td><label for="utf8">Text representation using UTF-8 characters (better displayed with fixed width fonts)</label></td></tr>
            </table>
        </div>

        <div class="section-wrapper">
            <a id="tutorial"></a>
            <div class="section tutorial hidden">
                <div class="close-section"><span onclick="hideTutorial()">⨯</span></div>
                <h3>Tutorial</h3>
                <div class="subsection">
                    <p>
                        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).
                    </p>
                    <p>
                        Click on a formula or its orthogonal to apply the <span class="bold">axiom rule</span>.
                    </p>
                    <div class="proof-container">{"s":{"cons":[{"t":"litt","v":"A"},{"t":"dual","v":{"t":"litt","v":"A"}}]},"ar":null}</div>
                    <p>
                        If the two formulas are not explicitly orthogonal, you can click on <span class="bold">thesis symbol</span> to attempt to apply the axiom rule on a two-formulas sequent.
                    </p>
                    <div class="proof-container">{"s":{"cons":[{"t":"one"},{"t":"bottom"}]},"ar":null}</div>
                    <p>
                        Click on <span class="bold">connectives</span> to apply the associated rules.
                    </p>
                    <div class="proof-container">{"s":{"cons":[{"t":"par","v1":{"t":"litt","v":"A"},"v2":{"t":"dual","v":{"t":"litt","v":"A"}}}]},"ar":null}</div>
                    <p>
                        <span class="bold">Move formulas</span> within the list before applying <span class="bold">tensor rule</span>.
                            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.
                    </p>
                    <div class="proof-container">{"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}</div>
                    <p>
                        As for <span class="bold">plus rules</span>, just click on the left or right sub-formula.
                    </p>
                    <div class="proof-container">{"s":{"cons":[{"t":"litt","v":"A"},{"t":"plus","v1":{"t":"litt","v":"B"},"v2":{"t":"dual","v":{"t":"litt","v":"A"}}}]},"ar":null}</div>
                    <p>
                        For the <span class="bold">whynot</span> connective, you have three possibilities:
                    </p>
                    <ul><li>single click on whynot connective applies <span class="bold">weakening</span></li>
                        <li>single click on the sub-formula applies <span class="bold">dereliction</span></li>
                        <li>double click applies <span class="bold">contraction</span>.</li>
                    </ul>
                    <div class="proof-container">{"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}</div>
                    <p>
                        <span class="bold">That's it!</span> Here are some extra examples for you to prove. Have fun!
                    </p>
                    <ul class="examples">
                        <li><a href="/?s=A%E2%8A%97B+%E2%8A%A2+B%E2%8A%97A">A⊗B ⊢ B⊗A</a></li>
                        <li><a href="/?s=%28A%E2%8A%97B%29%E2%8A%97C+%E2%8A%A2+A%E2%8A%97%28B%E2%8A%97C%29">(A⊗B)⊗C ⊢ A⊗(B⊗C)</a></li>
                        <li><a href="/?s=A%E2%8A%97%28B%E2%8A%B8C%29+%E2%8A%A2+B%E2%8A%B8%28A%E2%8A%97C%29">A⊗(B⊸C) ⊢ B⊸(A⊗C)</a></li>
                        <li><a href="/?s=A%E2%8A%97%28B%E2%8A%95C%29+%E2%8A%A2+%28A%E2%8A%97B%29%E2%8A%95%28A%E2%8A%97C%29">A⊗(B⊕C) ⊢ (A⊗B)⊕(A⊗C)</a></li>
                        <li><a href="/?s=%21A%E2%8A%97%21B+%E2%8A%A2+%21%28A%E2%8A%97B%29">!A⊗!B ⊢ !(A⊗B)</a></li>
                        <li><a href="/?s=%21%28A%26B%29+%E2%8A%A2+%21A%E2%8A%97%21B">!(A&amp;B) ⊢ !A⊗!B</a></li>
                        <li><a href="/?s=%21A%E2%8A%97%21B%E2%8A%A2%21%28A%26B%29">!A⊗!B ⊢ !(A&amp;B)</a></li>
                    </ul>
		    <p>You can play with <a href="https://github.com/etiennecallies/click-and-collect/wiki/Examples">yet another list of examples</a> if you want.</p>
                </div>
            </div>
        </div>

        <div class="section-wrapper darker-gray">
            <a id="rules"></a>
            <div class="section rules hidden">
                <div class="close-section"><span onclick="hideRules()">⨯</span></div>
                <h3>Derivation rules</h3>
                <div class="row">
                    <div class="proof-container">{"s":{"cons":[{"t":"litt","v":"A"},{"t":"dual","v":{"t":"litt","v":"A"}}]},"ar":{"rr":{"r":"axiom"},"p":[]}}</div>
                </div>
                <div class="row">
                    <div class="proof-container">{"s":{"cons":[{"t":"one"}]},"ar":{"rr":{"r":"one"},"p":[]}}</div>
                    <div class="proof-container">{"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}]}}</div>
                    <div class="proof-container">{"s":{"cons":[{"t":"litt","v":"Γ"},{"t":"top"},{"t":"litt","v":"Δ"}]},"ar":{"rr":{"r":"top","fp":1},"p":[]}}</div>
                </div>
                <div class="row">
                    <div class="proof-container">{"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}]}}</div>
                    <div class="proof-container">{"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}]}}</div>
                </div>
                <div class="row">
                    <div class="proof-container">{"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}]}}</div>
                </div>
                <div class="row">
                    <div class="proof-container">{"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}]}}</div>
                    <div class="proof-container">{"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}]}}</div>
                </div>
                <div class="row">
                    <div class="proof-container">{"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}]}}</div>
                </div>
                <div class="row">
                    <div class="proof-container">{"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}]}}</div>
                    <div class="proof-container">{"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}]}}</div>
                    <div class="proof-container">{"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}]}}</div>
                </div>
                <div class="row">
                    <div class="proof-container">{"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}]}}</div>
                </div>
            </div>
        </div>


        <div class="section-wrapper dark-gray">
            <div class="section footer">
                <div class="subsection">
                    <a href="https://github.com/etiennecallies/click-and-collect/wiki">
                        <img src="static/images/github-icon.svg" title="View source code and additional informations" height="25" width="25"/>
                    </a>
                </div>
                <div class="subsection">
                    <p>This tool design was mainly inspired by <a href="http://logitext.mit.edu/">Logitext</a>.</p>
                </div>
            </div>
        </div>
    </body>
</html>
