Homework (May 16th)

Master / Vertiefung Logikbasierte Wissensrepräsentation
1

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.

2

Homework (May 16th)

  1. Implement the missing proof rules for a full natural deduction calculus, following the rules in https://new.kwarc.info/teaching/AI/slides.pdf
  2. Prove the SCombinator in PLSyntax
3

The SCombinator we defined in the lab seems to be missing a bracket due to ⟹ not being defined as right associative, i.e.
(P ⟹ (Q ⟹ R)) ⟹ (P ⟹ Q) ⟹ (P ⟹ R) should actually be (P ⟹ (Q ⟹ R)) ⟹ ((P ⟹ Q) ⟹ (P ⟹ R))

Otherwise you cannot prove the homework.

4

Urgh, yes, sorry, I’m so used to the function arrow being right-associative that I didn’t even think that the other one might not be…:smiley: