Computer Mathematics and Proof Theory Summer School


Date
07/08/2013 - 07/11/2013
Location
NIMS
컴퓨터 수학과 증명론 여름학교 날 짜 : 2013년 7월 8일 ~ 7월 11일 장 소 : 국가수리과학연구소, 대전 여름학교 소개 수리논리와 증명보조기(proof assistants)의 발전을 통해 수학적 개념과 증명을 일종의 컴퓨터 프로그램처럼 다룰 수 있게 되었다. 예를 들어, 2005년 Georges Gonthier가 Coq이라는 증명보조기 프로그램을 이용하여 4색정리를 재증명하였으며, 이는 Kenneth Appel과 Wolgang Haken의 100% 검증되지 않았던 1976년 증명이 옳음을 보여주는 것이다.또한 2012년에는 Feit-Thompson Theorem 또한 Georges Gonthier에 의해 Coq으로 재증명되었다. 위 두 예제는 컴퓨터 알고리즘을 이용한 계산뿐만 아니라 수학적 증명도Coq과 같은 컴퓨터 프로그램으로 다룰 수 있음을 반증한다.이와같이 컴퓨터를 이용하여 수학적 연구를 진행하는 분야를 컴퓨터수학이라 하며 이미 수학 및 전산학의 다양한 연구분야에서 활용되고 있다. 이러한 성과는 부분적으로는 힐버트, 괴델, 튜링 등에 의해 발전된 증명론과 계산이론 분야에서의 뛰어난 업적에 기반한다. 이번 여름학교에서는 증명론의 발전과정을 되새기고, 증명론의 기초를 다지며, 컴퓨터수학의 활용을 배울 수 있는 기회를 제공하고자 한다.본 여름학교는 대한수리논리학회를 중심으로 대한수학회, 한국정보과학회, 한국논리학회 등이 참여하고 NIMS가 지원하는 매우 뜻 깊은 연합 학술대회 성격의 여름학교이다.
img2

여름학교 방배정:
여름학교 안내: