Not logged in. · Lost password · Register

Jazzpirate
Member since Oct 2016
767 posts
Subject: 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
Fredy
Member since Jan 2019
6 posts
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.
Jazzpirate
Member since Oct 2016
767 posts
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...:D
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen