초록 ▼

□ 연구개요
본 연구는 수리논리 프로그래밍 언어인 증명보조기 Coq을 활용하여 수학자들이 쉽게 배우고 다룰 수 있는 행렬 계산기와 선형대수 증명보조 프로그래밍 도구를 개발하는 것이 기존 목표였다. 이 주제는 이미 유럽 등지 에서 활용하는 수리논리 프로그래밍 언어를 국내의 연구 도구로 활용하여 진행한다는 데에서 의미를 지니며, 국내 수학의 발전과 대중화 및 연구 분야의 다양화를 이끌어낸다는 점에서도 매우 중요한 연구이다.

□ 연구 목표대비 연구결과
기존 달성 목표는 1차 년도에 기초 대수 패키지 확보, 2차 년

□ 연구개요
본 연구는 수리논리 프로그래밍 언어인 증명보조기 Coq을 활용하여 수학자들이 쉽게 배우고 다룰 수 있는 행렬 계산기와 선형대수 증명보조 프로그래밍 도구를 개발하는 것이 기존 목표였다. 이 주제는 이미 유럽 등지 에서 활용하는 수리논리 프로그래밍 언어를 국내의 연구 도구로 활용하여 진행한다는 데에서 의미를 지니며, 국내 수학의 발전과 대중화 및 연구 분야의 다양화를 이끌어낸다는 점에서도 매우 중요한 연구이다.

□ 연구 목표대비 연구결과
기존 달성 목표는 1차 년도에 기초 대수 패키지 확보, 2차 년도에는 선형대수의 주요 정리를 컴퓨터 프로그램으로 구현하고, 3차 년도에는 1, 2차년도의 연구 성과를 토대로 행렬 분해 알고리즘을 구현 및 다양한 대수구조로의 확대 적용이었다. 3차년도에는 선형대수학을 공부하면서 빠지지 않고 다루게 되는 QR-분해 및 SVD 등을 구현하는 것이 최종 연구 목표였다. 하지만 현재 기초 대수 패키지 확보가 아직 진행 중이고, 1차 년도에 수학의 메타논리를 본 연구의 구현 도구인 Coq을 활용하여 수행한 논문을 출판하였다.

□ 연구개발결과의 중요성
아직은 가시적 결과가 뚜렷하게 나타난 것은 없지만, 후속 연구를 지속적으로 진행하여 수리논리를 바탕으로 한 선형대수 행렬계산기, 나아가서는 수학교육교구 개발이 달성된다면 수학적 연구의 다양화와 더불어 수리논리 능력과 컴퓨터 프로그래밍 능력의 향상이 가능하다는 관점에서 수학교육분야로도 충분히 그 가치가 있다고 판단된다.

(출처 : 연구결과 요약문 3p)

목차 Contents

• 표지 ... 1
• 연구결과 요약문 ... 3
• 목차 ... 4
• 1. 연구개발과제의 개요 ... 5
• 2. 연구수행내용 및 연구결과 ... 5
• 3. 연구개발결과의 중요성 ... 6
• 4. 참고문헌 ... 7
• 5. 연구성과 ... 7
• 대표적 연구실적 ... 8
• 끝페이지 ... 12