이전 주제 보기 :: 다음 주제 보기 |
글쓴이 |
메시지 |
손님
|
올려짐: 2005년10월3일 20:08 주제: 숙제에서요.. |
|
|
1. 4번 문제가 잘 이해 안가서 그러는데 program으로 바꾸라 함은
어찌 되는 것인지요.. 예 하나만 들어주시면 쉽게 풀수 있을듯...
2. 5번 문제는 책에 있는 방식으로 풀어야 하나요? 아님 수업시간에 배운
Curry-Howard isomorphism으로 풀어도 되나요?
어렵습니다. ㅠㅠ |
|
위로 |
|
|
정영범
가입: 2005년 9월 5일 올린 글: 167
|
올려짐: 2005년10월4일 12:32 주제: |
|
|
(p -> q) & p -> q
위의 명제를 증명한다고 할 때
입력은 (p -> q) & p 이고 결과는 q 라고 생각하시면 됩니다.
이에 해당되는 프로그램은
lambda f. (f.1 f.2) 가 되겠죠.
f = (p -> q, p)
f.1 = p -> q
f.2 = p
(f.1 f.2) = q
아시겠죠?
알고보면 숙제의 답도 간단하게 나옵니다. |
|
위로 |
|
|
황의권
가입: 2005년 9월 5일 올린 글: 105
|
올려짐: 2005년10월4일 14:41 주제: Re: 숙제에서요.. |
|
|
수강생 씀: | 5번 문제는 책에 있는 방식으로 풀어야 하나요? 아님 수업시간에 배운
Curry-Howard isomorphism으로 풀어도 되나요?
|
문제에서 Gentzen system 안에서 증명하라 하였으므로 그에 따라서 해보세요 |
|
위로 |
|
|
손님
|
올려짐: 2005년10월4일 15:47 주제: |
|
|
읽기자료에서는 Gentzen's natural deduction 이 수업시간에 배운
Curry-Howard와 일치하는데 상관없는 것 아닌가요?
책에 있는 방법은 이해하기가 조금 어렵던데요 |
|
위로 |
|
|
황의권
가입: 2005년 9월 5일 올린 글: 105
|
올려짐: 2005년10월4일 19:51 주제: |
|
|
curry-howard isomorphism과 Gentzen system이 같다는 것을 '보인 후' curry-howard isomorphism을 사용하셔도 무방합니다.
예제 3.3과 3.4의 notation은 물론 이해하기 어렵겠지요. 그러니 예제 3.5(교재 46page)에 있는 tree를 참조하세요.
덧붙이면. 실명 사용을 '강력하게' 권장합니다 ^-^ |
|
위로 |
|
|
황의권
가입: 2005년 9월 5일 올린 글: 105
|
올려짐: 2005년10월5일 13:21 주제: |
|
|
예제 3.5에서의 tree는 2단원에서의 semantic tableau에 관한 부분을 참조해주세요. 그러한 방식으로 답을 기술하시면 됩니다. |
|
위로 |
|
|
홍원욱 손님
|
올려짐: 2005년10월6일 0:30 주제: Gentzen System을 사용하는데 있어서... |
|
|
교과서 1-2번문제를 푸는데요
증명: ㅏA->B ->( ( ~A->B) ->B)
1) Axiom1: A,~A,B
2) alpha -> rule에 의해 : ~A, A->B
3) Axiom2: B,~B
4) 2)와 3)을 beta -> rule에 의해 : ~A, B, ~( (A->B) -> B )
5) 4)와 alpha -> rule에 의해 : A->B, ~( (A->B) -> B )
6) 5)와 beta -> rule에 의해 : ~((A->B) -> ( (A->B) -> B ) )
이렇게 해버리니 증명이 아니라 반례를 만들어버렸는데...
어디서 잘못되었는지 모르겠습니다.
Gentzen의 beta룰이 책에 보면 U1 union {b1} 과 U2 union {b2} 가
U1 union U2 union {b}로 된다고 되어 있는데, 제가 적용을 잘못한 것인지요.. |
|
위로 |
|
|
홍원욱 손님
|
올려짐: 2005년10월6일 0:36 주제: |
|
|
앗 위에서 오타를 냈습니다.
2) alpha -> rule에 의해 : ~A, A->B
가 아니라
2) alpha -> rule에 의해 : ~A, ~A->B 입니다. |
|
위로 |
|
|
홍원욱
가입: 2005년 10월 6일 올린 글: 1
|
올려짐: 2005년10월6일 0:42 주제: |
|
|
이런 완전히 오타로 도배를 했군요..
~A->B라고 써야 하는 부분을 A->B로 써버렸습니다.
제가 원래 의도한 글은 :
증명: ㅏA->B ->( ( ~A->B) ->B)
1) Axiom1: A,~A,B
2) alpha -> rule에 의해 : ~A, ~A->B
3) Axiom2: B,~B
4) 2)와 3)을 beta -> rule에 의해 : ~A, B, ~( (~A->B) -> B )
5) 4)와 alpha -> rule에 의해 : A->B, ~( (~A->B) -> B )
6) 5)와 beta -> rule에 의해 : ~((A->B) -> ( (~A->B) -> B ) ) |
|
위로 |
|
|
황의권
가입: 2005년 9월 5일 올린 글: 105
|
올려짐: 2005년10월6일 0:54 주제: |
|
|
교재 내의 Gentzen System 부분에 보면,
인용: | ├ A in G if and only if there is a closed semantic tableau for ¬A |
이라는 말이 있습니다. 지금 교재가 옆에 없어 G의 rule에 맞게 되었는지 확인해드리지는 못 하겠지만 위의 보조정리를 참고해주세요
붙임: semantic tableau를 그리며 따라가는 것이 더 편하지 않을까요? |
|
위로 |
|
|
|