MAT8070-01 (2014학년도 1학기)

2014-01-20 18:33:23  2014-01-21 14:57:05 
논리학특강 I 
과225  금6,7,8 

coq-hurry.pdf (308991 Bytes)

lambda-sel.pdf (149676 Bytes)

typetheorie-sel.pdf (90705 Bytes)
 
이계식  이과대학 수학 
  010-2074-5742 
leegys@hknu.ac.kr
 
+ 컴퓨터수학에 관심 있는 학부생 및 대학원생현대수학의발전과수학,논리,
+ 기초적인수학적마인드만 있으면 누구나 참여 가능
1) 강의 부제목: 컴퓨터를 이용하여 증명하기

2) 수업목표
1980년대부터 현대 수학사에서 가장 핫한 이슈로 떠오른 분야가 증명보조기(proof 
assistants) 연구이다. 본 강의에서는 Coq(콕)이라는 증명보조기를 학습하는 과정을 통
해 컴퓨터 프로그램이 일반 수학자들이 일상적으로 행하는 수학 증명을 위해 어떻게 활용
될 수 있는가를 보여주고자 한다. 참여하는 학생들은 강의를 통해 현대 수학의 발전 내용
을 보면서 수리논리, 수학 및 컴퓨터가 어떻게 조화를 이룰 수 있는지 확인할 수 있다.

3) 수업개요
강의에서 다루는 내용은 아래와 같다.

 + 람다해석학(Lambda Calculus) 기초
 + 유형론(Type Theory) 기초
 + Coq 증명보조기 소개
 + 컴퓨터를 이용한 수학적 검증(Verification) 기초
 + 증명론 기초
 + Coq 증명보조기를 이용한 프로그래밍
필수는 아니며 아래 과목을 추천함.
1) 학부수준의 선형대수, 미적분학 
2) 수리논리 입문 과목
3) 학부 수준의 프로그래밍 입문 관련 과목
1) 슬라이드 이용 일반 강의와 컴퓨터 이용 실습 병행.
2) 강의시간에 노트북을 이용 권유, 하지만 필수는 아님.
3) 과제는 컴퓨터를 반드시 이용하는 경우 발생.
1) 중간/기말고사 (60%)
2) 과제 평가 (30%)
3) 출석(10%)
특정 교재 없으며 강의에 필요한 자료는 수업 시간에 파일로 배부될 것임.
참고 사이트:
1) Coq 프로그램: http://coq.inria.fr/
2) ProofWeb webinterface: http://prover.cs.ru.nl
3) Coq in a hurry: http://cel.archives-ouvertes.fr/docs/00/45/91/39/PDF/coq-
hurry.pdf
4) 관련 강의 사이트: http://www.cs.ru.nl/H.Geuvers/onderwijs/provingwithCA/
소속: 한경대학교 컴퓨터웹정보공학과 교수, 연세대 수학과 외래강사
홈페이지: http://formal.hknu.ac.kr/
주전공: 수리논리, 컴퓨터논리, 증명론, 유형론, 증명보조기
추후 결정.
1) Goal
We introduce a proof assistant Coq which plays an important role in the 
history of modern mathematics. We can use Coq to do everyday mathematics as 
traditional mathematicians do. The participants will learn how one can combine 
mathematical logic, mathematics, anc computer for a usuful use in doing 
everyday mathematics.

2) Introduction - The main contents will be the following:

 + basics of lambda calculus
 + basics of type theory
 + introduction of the proof assistant Coq
 + Verification of mathematical proofs by Coq
 + basics of proof theory
 + programming using Coq
2014-03-03 2014-03-09
과목 소개: 증명보조기, 검증, 논리, 유형
론, Formulas-as-types, Coq 
강의 내용 관련 과제 
(3.3)개강 (3.5 - 3.7) 수강신청 확인 및 변경 
2014-03-10 2014-03-16
1) Simple type theory
2) 명제논리와 formulas-as-types 
강의 내용 관련 과제 
 
2014-03-17 2014-03-23
Curry 형식 simple type theory 
강의 내용 관련 과제 
 
2014-03-24 2014-03-30
Polymorphic types 
강의 내용 관련 과제 
 
2014-03-31 2014-04-06
Dependent type theory 
강의 내용 관련 과제 
(4.2- 4.4) 수강철회 
2014-04-07 2014-04-13
Natural deduction in Coq 
강의 내용 관련 과제 
(4.9) 학기 1/3선 
2014-04-14 2014-04-20
중간시험 
중간시험 및 평가 
(4.17 - 4.23) 중간시험 
2014-04-21 2014-04-27
Inductive types in Coq 
강의 내용 관련 과제 
(4.17 - 4.23) 중간시험 
2014-04-28 2014-05-04
Recursion in Coq 
강의 내용 관련 과제 
 
10  2014-05-05 2014-05-11
1) Higher order logic
2) Calculus of Constructions 
강의 내용 관련 과제 
(5.5)어린이날 (5.6) 석가탄신일(5.10) 창립기념일 
11  2014-05-12 2014-05-18
Programming with dependent inductive 
types 
강의 내용 관련 과제 
(5.16) 학기 2/3 선 
12  2014-05-19 2014-05-25
Coq의 다양한 특징 소개 및 고급 이용 기술 
강의 내용 관련 과제 
 
13  2014-05-26 2014-06-01
Coq 고급 이론 및 기술 
강의 내용 관련 과제 
 
14  2014-06-02 2014-06-08
Coq 이용 문제해결 연습 
강의 내용 관련 과제 
(6.6) 현충일 
15  2014-06-09 2014-06-15
기말시험 연습 및 자율학습 
기말시험 예비 문제 
(6.9 - 6.21) 자율학습 및 기말시험 
16  2014-06-16 2014-06-22
기말시험 
기말시험 및 평가 
(6.9 - 6.21) 자율학습 및 기말시험