Exercises rely on the C1ick ⅋ c⊗LLec⊥ interactive proof system for manipulating sequent calculus proofs of Linear Logic.
Start by getting familiar with the system by using its tutorial (from "
Here is a short tutorial" to "
That's it!": skip the final 7 examples).
You can then either replay the examples given in Michele Pagani's lecture:
or move to the Linear Logic Tutorial (be careful: some proposed sequents are not provable!).
Prove that if you have 35€ and you go to Michele's restaurant, you can get Vin, 2 verres d'Eau, Quiche, Canard and Raisin, if it is definitely not a good season for bananas and oranges.
Menu à 35 euros Entrée : Quiche Lorraine ou Saumon Fumé et Plat : Pot-au-Feu ou Filet de Canard et Dessert : un fruit selon la saison (Banane ou Raisin ou Oranges) ou un gâteau (Tarte aux Pommes ou Mille-Feuilles) Vin et Eau à volonté !
Play with reduction steps: try to predict the result before asking the machine to reduce the cut.
Then you can use the
↶/↷ buttons to replay.
Key cases: ax, ⊗/⅋, ⊕1/&, ⊕2/&, 1/⊥, !/?d, !/?c, !/?w
Commutation cases: ⊗, ⅋, ⊕1, ⊕2, &, ⊥, ⊤, ! (including !/!), ?d, ?c, ?w
Booleans can be encoded in LL as additive Booleans 1⊕1. This means that there are exactly two cut-free proofs of this formula which are chosen as representing
─── 1 ─── 1 ⊢ 1 ⊢ 1 ─────── ⊕1 and ─────── ⊕2 ⊢ 1 ⊕ 1 ⊢ 1 ⊕ 1
A function from Booleans to Booleans can then be encoded as a proof of 1⊕1 ⊢ 1⊕1 or equivalently of ⊢ ⊥&⊥, 1⊕1, meaning that when it is cut against the encoding of an input it reduces (by cut-elimination) to the encoding of the output.
Using the links below you get a partial proof with a cut: you should complete the right-hand side according to the function you want to encode and you can test it then by filling the left part(s).
Try to get two different cut-free proofs by reducing the cut in the following proofs:
By reducing the cuts in differents ways obtain two proofs which differ by commutation of rules (as shown in the
MLL proof nets lecture):
Reduce the following cut step-by-step to see how it is able to search for the ⅋ rule inside the proof and to erase it: ⅋ eraser.
Reduce the following cut to move the ! rule down in the proof: ! down.
A proof of a formula !A can be duplicated by cut elimination: !A duplicator. Follow it step-by-step.
You can continue with additional examples.
You can investigate MLL as a Lego game.