Constructive Logic

공부 2009.09.22 14:57
일반적인 classical logic에서는 not not A가 A라는게 성립하는데

constructive logic에서는 그게 성립하지 않는다.

그러한 '사실' 은 알고있었는데 왜 그런지는 모르고 있다가

오늘 전산논리 수업덕분에 알게 되었다. 늦게라도 가길 잘한듯.


이유는 '∃'(어떤) 와 'V'(disjunction, or) 때문인데

constructive logic에서는 ∃x 가 존재하는것이 참임을 증명할때

그 x 를 명확히 지정해야하고

A or B 가 참이라는것을 증명하려면

A와 B중에 어떤게 참인지 지정해야 하기 때문이다.


예를들면 (not A) or A 는 classical logic에서는 항상 참이지만

constructive logic에서는 A를 모를 수도 있기 때문에 참이 아니다.


이런 설정은 기존의 classical logic에 비해 상당히 귀찮은 문제들을 만들어내는데,

그럼에도 불구하고 이렇게 하는 이유는

1. constructive logic을 이용한 proof으로부터 program을 추출할 수 있고

2. constructive logic이 classical logic보다 강력(포함)하기 때문이라네.


함수형 프로그래밍 언어에서 보여주는 독특하고 강력한 기능들이

전산논리 수업과 어떻게 연관이 되는지 조금씩 느낌이 오는것 같다.

'공부' 카테고리의 다른 글

Google Summer of Code2010 & CGAL  (0) 2010.03.30
O/R mapping  (0) 2010.02.26
Laplacian Pyramid on GPU  (1) 2010.01.13
Block-based Web Search  (0) 2009.12.06
오토 레포트  (3) 2009.11.04
Constructive Logic  (3) 2009.09.22
Posted by youknow04

댓글을 달아 주세요

  1. 희제 2009.09.22 21:59  댓글주소  수정/삭제  댓글쓰기

    그래서 왜 not not A = A(1)가 성립하지 않는건데?
    아래 설명은 전부 (not A) or A = true(2)가 성립하지 않는다는것에 대한 설명 아닌가?
    (1)과 (2)가 동치인가?

    • youknow04 2009.09.26 13:37  댓글주소  수정/삭제

      예를들어 A가 이방의 모든 사람은 한국인이다 일때
      not A는 이방의 어떤 사람은 한국인이 아니다 인데
      A가 거짓이더라도 not A가 참이 아닐 수도 있는게
      not A를 보이려면 '어떤' 사람이 한국인이 아닌지를 정해야하는데
      방에 사실 아무도 없거나 하면 그럴 수가 없잖아?

      이런식으로 '어떤'하고 'or' 때문에 A가 거짓이더라도 not A가 반드시 참이 되는게 아니라서, 클래시컬 로직에서처럼 not not A가 A가 아니라는 거였는데,

      지금보니까 너말데로 왜 not not A = A가 참인지는 본문에 설명이 없네...ㅎㅎ
      그리고 공부도 좀 더 해야겠다.
      댓글달면서 생각해보니 내가 제대로 알고있는건가 하는 생각이 드네.

  2. Euryale 2010.01.18 19:04  댓글주소  수정/삭제  댓글쓰기

    저도 대학에 들어가면 전산논리수업을 받아봐야겠네요

귀국

일상 2009.09.04 16:47
베를린대학에서 약2주가량 공동연구 하다가 돌아왔다.
유레일 패스 끊어가서 사이사이 주말마다 돌아다니면서 여행도 할 수 있었고,
교수님이 많이 지원해주셔서 돈도 별로 안들었고,
연구결과도 괜찮았고, 바람직한 출국이었음.

이번에 새로가본곳은

벨기에-브뤼셀
네덜란드-암스테르담
룩셈부르크-룩셈부르크시티
오스트리아-빈(비엔나)
독일-베를린
독일-프랑크푸르트

기존에 가본곳까지 추가해서 지도에 찍어보면

이제 13개국정도 가본듯하다.

다음에 출국할일 있으면 잘사는 나라 말고
다른곳에도 한번 가보고 싶다.

최근에 논문내려던 학회가 말레이시아쪽에서 열려서 기대했었는데,
정리하다보니 내 결과가 틀려서 못냈던게 다시 생각나면서 좀 아쉬워진다.

'일상' 카테고리의 다른 글

티스토리로 블로그 이전  (0) 2010.05.11
AAAC2010  (0) 2010.04.18
일본여행  (0) 2010.02.08
귀국  (0) 2009.09.04
IEEE 인공지능 대회  (0) 2009.08.08
블로그 시작~  (2) 2009.07.28
Posted by youknow04

댓글을 달아 주세요

IEEE 인공지능 대회

일상 2009.08.08 00:25
전자전기관련 세계 최대의 기술조직인 IEEE에서
슈퍼마리오 인공지능대회를 개최한다.

상금은 500불(75만원정도?)라서
최근 신청한 올엠인공지능대회 상금(300만원)에도 못미치지만
상금보다도

"Winner of IEEE AI competition"

...이라는 무지무지하게 값진 타이틀 때문에 정말 많이 끌리더라.

하지만 내가 대회를 너무 늦게 알아서 시간도 촉박하고,
일정에 출국이랑 논문듀랑 올엠 인공지능 대회까지 이미 걸려있어서 참가를 포기했다.

근데 오늘 찾아보니 유튜브에 이미 누가 구현한게 올라와 있더라.



이정도면 잘하는거긴 하지만,
그냥 기본 전략을 앞으로 빨리 가는식으로 해놓고,
매순간의 게임트리 돌리고 결과를 적절히 재사용하는 식으로 짜면
나도 저정도는 어렵지 않을것 같았다.

근데 아래의 동영상(좀 더 어려운 레벨을 슬로우로 돌린것)을 보고나서, 역시 세계의 벽이란건 그리 호락호락 하지 않구나라는 생각이 들더라.



그러고보면 나는 POSTECH, KAIST, 서울대 이렇게 세 학교의 학생들 말고는 저런 대회를 같이 해본적이 없어서,
외부의 인공지능 대회는 수준이 어느정도나 될지 잘 모르겠다는 생각이 다시 들면서
올엠 인공지능 대회도 엄청난 괴수들이 나올까봐 불안불안해졌다.
상금 꼭 타야하는데...

'일상' 카테고리의 다른 글

티스토리로 블로그 이전  (0) 2010.05.11
AAAC2010  (0) 2010.04.18
일본여행  (0) 2010.02.08
귀국  (0) 2009.09.04
IEEE 인공지능 대회  (0) 2009.08.08
블로그 시작~  (2) 2009.07.28
Posted by youknow04

댓글을 달아 주세요