9 0 0 0 OA 定理証明支援系に基づく形式検証 -近年の実例の紹介とCoq入門-
- 著者
- アフェルト レナルド
- 雑誌
- 情報処理
- 巻号頁・発行日
- vol.55, no.5, pp.482-491, 2014-04-15
近年,定理証明支援系による成功が続いている:数学の証明の形式化,コンパイラやオペレーティングシステムの検証,などである.近年,定理証明支援系が数学とセキュアなコンピュータシステムの構築に欠かせないツールになってきており,本稿では,定理証明支援系による実例を紹介し,代表的な定理証明支援系Coqの基本的な使い方を説明する.
2 0 0 0 OA Mathematical Components入門
- 著者
- アフェルト レナルド
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.34, no.2, pp.2_64-2_74, 2017-04-26 (Released:2017-06-26)
コンピュータのプログラムと数学の証明の間に密な関係があることはよく知られている.1969年に発見されたCurry-Howard同型対応により,プログラムの型を言明(statement)として見れば,プログラム自体はその言明の証明として見られる.これにより,数学の証明の検査はプログラムの型付けに帰着する.この発想に基づいて,定理証明支援系という検証ツールの開発が行われてきた.近年,定理証明支援系を用いて,ようやく現実的なプログラムと証明の検証が可能となっている.現実的な証明の一例として,2005年から2012年までマイクロソフト・INRIAの共同研究組織で形式化された奇数位数定理が挙げられる.奇数位数定理は膨大な証明により示された重要な群論の定理であるため,その形式化は大きなマイルストーンとなっている.加えて,その形式化の基盤であるMathematical Componentsもまた,形式数学におけるライブラリとして重要な成果である.我々のデジタル社会を支える基本的なコンピュータプログラムであるRSA暗号や楕円曲線暗号や符号などは,整数論や群論や線形代数などの数学に基づいているが,Mathematical Componentsを用いることで,これらのプログラムの厳密な仕様の記述ができるようになった.しかし,Mathematical Componentsのような大規模なライブラリの利用には専門知識が不可欠である.本解説では,Mathematical Componentsによる形式化を紹介する.群論のラグランジュ定理を用いて,そのライブラリの基本的な使い方を説明する.