Hier werden in unregelmäßigen Abständen Aufgaben zum Vorlesungsstoff gestellt werden ...


Aufgabe 1

Hilbertscher Kalkül der klassischen Aussagenlogik:

Axiomenschemata
T
A → (B → A)
(A → B ) → ((A → (B → C )) → ((A → C )))
¬(¬A) → A

Die einzige Regel ist der modus ponens.

Kann X ∨ ¬X im Hilbertschen Kalkül bewiesen werden?
Falls ja, wie?
Falls nein, warum nicht?

Aufgabe 2

Verwernden Sie den in der Vorlesung verteilten natürlichen Deduktionskalkül in Sequenzenform für die klassische Logik, um die DeMorganschen Gesetze zu beweisen.

Aufgabe 3

Zeigen Sie die Ableitbarkeit der Mix-Regel im Sequenzenkalkül LK.

Aufgabe 4

Vergleichen Sie die Typkalküle für lazy und eager evaluation.
Was zeichnet diese Kalküle aus?
Ist eine Kombination denkbar?

Aufgabe 5

Wenden Sie die Phasensemantik für lineare Logik anhand eines einfachen Beispiels einer LL-Tautologie an.