Assignment 2

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Assignment 2
Dear all,

I’ve uploaded an MMT file for assignment 2: https://gl.mathhub.info/Teaching/LBS2021/-/blob/main/source/assignment2.mmt
I haven’t solved it fully myself yet so it may still contain mistakes. If you see any mistakes, please let me know!

This is a very difficult homework assignment and we haven’t set a deadline yet.
Please try to understand as much as possible. For next Tuesday, we plan to have a lab session that is guided by your questions. So the more you prepare, the better.
In particular, please try to understand the provided proofs for andSwap, orIr and implI in part 2 so we can discuss any questions you have about them.
Note that I renamed the notations for the ND rules (because they somehow confused the parser).

You can solve the homework using the Jupyter GLIF kernel. Simply paste the code into one (or more) Jupyter cells.
That being said, there are certain advantages to using an IDE.
For that you have to install MMT on your machine. Here is the installation guide: https://uniformal.github.io//doc/setup/

Please reach out if you have any problems/questions.

Frederik


I’ve updated the assignment. There was one typo in [m]orIl[/m] and I’ve added a hint for [m]implE[/m].

Addendum
Dear all,

what I also should have mentioned:
To learn lambda calculus, you have to do it on paper.
I.e. you should try to solve the first part of the homework with pen-and-paper. You can enter (and type-check) your solutions in MMT but that’s just a way to submit it, not to actually work it out.

When I find some time, I’ll try to create a corresponding pdf assignment (like in e.g. the AI lecture).

Best
Frederik

IntelliJ Plugin
Hallo Jan Frederik,
ich habe auf meinem PC gerade versucht das MMT IntelliJ Plugin zu installieren, kann aber kein neues MMT Projekt erstellen. Bekomme die Fehlermeldung “Please select a valid MMT.jar (requires 20.0.0) or higher”, obwohl mit dem MMT.jar eigentlich alles in Ordnung sein sollte.

Ich verwende IntelliJ Community 2020.3 auf Windows 10.
Irgendeine Idee wie das sein kann (habe den ReflectionsCode im Plugin gerade angeschaut, die Klassen die er lädt gibt es alle), oder welche Version von IntelliJ sicher unterstützt wird?

Viele Grüße
Tobias


Das MMT IntelliJ Plugin hat ein paar bekannte Probleme mit IntelliJ 2020.3. So wie es scheint, ist ein Beheben eher zeitaufwändig und es gibt nur eine Person auf dieser Erde, die das am Effizientesten machen kann :smiley: (nicht ich)

Mit IntelliJ 2020.2 funktioniert es einwandfrei bei mir. Wenn du die IntelliJ Toolbox App installiert hast (sehr empfehlenswert), kannst du IntelliJ 2020.2 ganz einfach parallel zu deinem 2020.3 installieren lassen.

Ich benutze etwa 2020.3 zum Coden in Scala und 2020.2, um MMT-Formalisierungen zu editieren.

Respekt, dass du dich da durch den Code wühlst! :slight_smile:


Der Vollständigkeit halber:

Das MMT Plugin funktioniert mit IntelliJ 2020.2.4, MMT Plugin 20.0.0, Scala Plugin 2020.2.49. (Für die letzteren zwei Plugins sind das die neusten Versionen am heutigen Datum [2020-18-12]. Nur IntelliJ darf man nicht auf 2020.3 upgraden.)

1 „Gefällt mir“

Danke, mit 2020.2 hat es jetzt funktioniert :slight_smile:
Dann musste ich noch den Backend-Fehler beheben (https://fsi.cs.fau.de/forum/thread/17975-MMT-Bug) aber jetzt läuft es. Vielen Dank für die Infos!


FYI, es gibt nun eine neue MMT-Version (21.0.0) und eine neue MMT IntelliJ-Plugin Version (21.0.0)*. Die Kombination funktioniert dann auch mit dem neusten IntelliJ 2020.3.

*) Aktuell ist das Plugin noch unter Review bei JetBrains. In wenigen Werktagen sollte das Plugin jedoch auf dem Marketplace offiziell freigegeben sein.

1 „Gefällt mir“

In case someone wants some more to practice with:

reductioAdAbsurdum : {P,Q} ⊢P ⟶ ⊢(Q∧¬Q) ⟶ ⊢¬P ❙
modusPonens: {P, Q} (⊢P⇒Q) ⟶ ⊢P ⟶ ⊢Q  ❙
modusTollens: {P, Q} (⊢P⇒Q) ⟶ ⊢¬Q ⟶ ⊢¬P ❙

deMorgan1: {A,B} ⊢ ¬(¬A∧B) ⟶ ⊢(¬A∨¬B) ❙
deMorgan2: {A,B} ⊢ ¬(A∨B) ⟶ ⊢(¬A∧¬B) ❙

kontraPosition: {P, Q} ⊢P⇒Q ⟶ ⊢¬Q⇒¬P ❙

hypotheticalSyllogism: {P, Q, R} ⊢P⇒Q ⟶ ⊢Q⇒R ⟶ ⊢P⇒R ❙
conjunctivSyllogism: {P, Q} ⊢¬(P∧Q) ⟶ ⊢P ⟶ ⊢¬Q ❙
disjunctivSyllogism:  {P, Q} ⊢P∨Q ⟶ ⊢¬P ⟶ ⊢Q ❙

exFalsoQuodlibet: {P, Q} ⊢P∧¬P ⟶ ⊢Q❙
1 „Gefällt mir“