3. 강의목표
http://pl.postech.ac.kr/~gla/cs433/
This course covers the basics of logic in computer science. We study various styles of formulating logic, but the main focus of this course lies on a proof-theoretic study of constructive logic, as opposed to a model-theoretic study of classical logic. A proof-theoretic formalization of constructive logic serves as a foundation for type theory for programming languages, so this course should also be interesting to those interested in type theory. We also learn to program in a proof assistant Coq which enables us to formally write proofs in a logical language.
Topics to be covered include: propositional logic, natural deduction, normalization, Curry-Howard isomorphism, first-order logic, dependent types, sequent calculus, cut-elimination, classical logic, modal logic, substructural logic, and automated theorem proving.
4. 강의선수/수강필수사항
CSE-321 Programming Languages, or by permission of the instructor.
5. 성적평가
http://pl.postech.ac.kr/~gla/cs433/
7. 참고문헌 및 자료
http://pl.postech.ac.kr/~gla/cs433/
8. 강의진도계획
http://pl.postech.ac.kr/~gla/cs433/
11. 장애학생에 대한 학습지원 사항
- 수강 관련: 문자 통역(청각), 교과목 보조(발달), 노트필기(전 유형) 등
- 시험 관련: 시험시간 연장(필요시 전 유형), 시험지 확대 복사(시각) 등
- 기타 추가 요청사항 발생 시 장애학생지원센터(279-2434)로 요청