12/08/2020 Quiz (Week 9)
Logic Question 1
Quiz (Week 9)
Which one (or more) of expressions listed below is a possible formalisation of the phrase: Not all that glitters is gold.
1. ✗ 2. ✗ 3. ✔ 4. ✗
Question 2
Which of the expressions listed below is a possible formalisation of the Abraham Lincoln quote: You can fool all the people some of the time, and some of the people all the time, but you cannot fool all the people all the time.
1. ✗ 2. ✗ 3. ✗ 4. ✔ 5. ✗ 6. ✔
Question 3
Here is a proof of a logical statement in natural deduction style:
www.cse.unsw.edu.au/~cs3141/20T2/Week 09/quiz.html
1/4
)t ,p(looF .p∀ .t∀¬ ∧ ))t ,p(looF .p∃ .t∀( ∧ ))t ,p(looF .p∀ .t∃( ))t ,p(looF .t∀ .p∀ → eslaF( ∧ ))t ,p(looF .t∀ .p∃( ∧ ))t ,p(looF .t∃ .p∀( )t ,p(looF .t∀ .p∀¬ ∧ ))t ,p(looF .t∀ .p∃( ∧ ))t ,p(looF .t∃ .p∀( )t ,p(looF¬ .t∀ .p∀¬ ∧ ))t ,p(looF .t∀ .p∃( ∧ ))t ,p(looF .t∃ .p∀( )t ,p(looF¬ .t∃ .p∃ → ))t ,p(looF .t∀ .p∃( ∧ ))t ,p(looF .t∃ .p∀( ))t ,p(looF¬ ∧ )t ,p(looF( .t∀ .p∀
)))x(dloG → )x(rettilG(¬( .x∀ ))x(dloG → )x(rettilG( .x∀¬ ))x(dloG → ))x(rettilG(¬( .x∀ ))x(dloG → )x(rettilG( .x∃
12/08/2020 Quiz (Week 9)
The names of the rules used have been replaced with circled numbers. What is the rule used in each position?
1. ✗ 2. ✗ 3. ✗ 4. ✗ 5. ✔
Curry-Howard Correspondence Question 4
Selct all of the following types for which you can write a total, terminating Haskell function.
1. ✔
2. ✗
3. ✔
4.✗ ((a->c)->c)->a
Question 5
What is the computational interpretation of the theorem ?
1. ✔ The function that transforms a curried function to an uncurried one.
2. ✗ The function that transforms an uncurried function to a curried one.
3. ✗ The function that creates a tuple of the two given values and values. 4. ✗ There is no computational interpretation of this logical formula.
(a -> b) -> (b -> c) -> (a -> c)
((a, b) -> c) -> (a -> c)
(a -> c) -> ((a, b) -> c)
Question 6
www.cse.unsw.edu.au/~cs3141/20T2/Week 09/quiz.html
2/4
α1
β1
D ∨ C → )D → B( → )C → A( → B ∨ A D ∨ C → )D → B( → )C → A(
BA
E-→si 5 ;2I-∨si 4 ;1I-∨si E-∨si 5 ;2I-→si 4 ;1I-→si E-∨si 5 ;1I-→si 4 ;2I-→si
3 ;E-∨si 2 ;I-→si 1 3 ;E-→si 2 ;I-∨si 1 3 ;E-→si 2 ;I-∨si 1 3 ;E-∨si 2 ;I-→si 1 3 ;I-∨si 2 ;E-→si 1
E-→si 5 ;1I-∨si 4 ;2I-∨si I-→si 5 ;2E-∨si 4 ;1E-∨si
D ∨ C → )D → B( γ1 D∨C
)C → )B ∧ A(( → ))C → B( → A(
2δ; 1δ 2 D ∨ C D ∨ C B ∨ A 4D3Cα
5BD→B5AC→A 2δγ 1δβ
Q
12/08/2020 Quiz (Week 9)
Which of the following Haskell programs constitutes a valid proof of the theorem given in Question 3?
1. ✔
2. ✗ 3. ✗ 4. ✗ 5. ✗
Question 7
Below is a complicated proof that assuming
and , we can derive :
proof (Left a) f g = Left (f a)
proof (Right b) f g = Right (g b)
proof (a, b) f g = (f a, g b)
proof x f g = if x then f x else g x
proof x f g = x (f x) (g x)
proof (Left a) f g = Left (g a)
proof (Right b) f g = Right (f b)
What is the equivalent program to this proof, in typed lambda calculus (using Haskell-
style syntax for pairs)? Assume
1. ✗ 2. ✔ 3. ✗ 4. ✗ 5. ✗
and .
www.cse.unsw.edu.au/~cs3141/20T2/Week 09/quiz.html
3/4
E-→ B∧A
I-∧ A ∧ B I-→ )B ∧ A( → )A ∧ B(
B:b A:a
ABδI-∧ B∧A
B∧ABA
)b ,a( ))x dns ,x tsf( .xλ( ))b ,a( dns ,)b ,a( tsf( ))a ,b( tsf ,)a ,b( dns(
)a ,b( ))x tsf ,x dns( .xλ( )b ,a(
1E-∧ B 2E-∧ A δA∧B δA∧B
12/08/2020 Quiz (Week 9)
Question 8
What proof results from applying proof simpli cation as much as possible to the proof from Question 7?
1. ✗
2. ✗
3. ✔
4. ✗
5. ✗
Submission is already closed for this quiz. You can click here to check your submission (if any).
www.cse.unsw.edu.au/~cs3141/20T2/Week 09/quiz.html
4/4
I-∧
2E-∧
B∧A
I-∧
1E-∧
B∧A
I-∧
B∧A
B 1E-∧ A
I-∧ B ∧ A I-∧ B ∧ A BA BA
B 2E-∧ A
I-∧ A ∧ B I-∧ A ∧ B AB AB
I-∧ B ∧ A BA
B 2E-∧ A
I-∧ B∧A
1E-∧ B A
I-∧ A ∧ B AB
I-∧ A ∧ B AB