Developing a Proof Assistant Supporting an Improved Interaction Paradigm
개선된 대화 방식을 지원하는 증명도우미 개발하기
- 주제(키워드) Proof assistant , Interactive theorem prover , Type theory , Proof by pointing
- 발행기관 서강대학교 일반대학원
- 지도교수 박영재
- 발행년도 2009
- 학위수여년월 2009. 2
- 학위명 박사
- 실제URI http://www.dcollection.net/handler/sogang/000000044985
- 본문언어 영어
초록/요약
본 논문에서 저자는 보다 편리한 컴퓨터상에서의 대화식 정리증명을 위해 “point and choose”라 이름 붙여진 포괄적인 시각적 대화방식을 제안한다. 이 방식은 단지 특정 부분항을 지목한 후 그것에 적용할 수 있는 후보조작들 중에서 유망한 하나를 선택함에 의해 증명을 이루어 가는 것을 가능하게 해준다. 이 방식에서는 그간의 시각적 대화방식에서는 부분적이거나 개별적으로만 취급될 수 있었던 규칙적용, 다시쓰기, 귀납법과 같은 서로 다른 증명기법들이 완전하고도 통합적으로 취급될 수 있어 인간 기계간 대화가 보다 용이해진다. 이러한 생각을 시험하기 위해 저자는 실제 제안된 방식을 직접 지원하는 시범적인 프로그램을 타입이론에 기초하여 구현하였으며 몇몇 기초적인 수학이론을 이 프로그램 안에서 성공적으로 재구성하였다. 저자는 본 논문에서 이 새로운 증명도우미 프로그램이 어떤 식으로 개발되었는지를 적당한 수준에서 보고하며 이 안에서 그러한 수학이론들이 어떻게 형식화되었는지를 보인다.
more초록/요약
In this thesis, the author proposes a comprehensive graphical interaction paradigm named "point and choose" for more convenient interactive theorem proving on computers. This paradigm enables to guide the proof building process by pointing at a subterm and choosing a promising operation among the several ones that are possible for the subterm. In this paradigm, different proof techniques like rule application, rewriting and induction, that could be handled only partially and individually in existing graphical interaction paradigms, can be handled in a complete and integrated manner, and hence the man-machine interaction is made simpler. To test the idea, a tentative system that directly supports the proposed paradigm has been implemented based on a dependent type theory and some fundamental mathematical theories have been successfully reconstructed in this system. In this thesis, the author reports in some detail how this new proof assistant has been developed and shows how those mathematical theories has been formalized in it.
more