「形式的体系の定理証明支援系上での実現法」資料
第3回システム検証の科学技術シンポジウム
(2006.10.30-11.01)
における以下のチュートリアル
で使用した資料が
ダウンロードできます．
- タイトル 「形式的体系の定理証明支援系上での実現法」
- 著者 木下佳樹、高橋孝一、田辺良則、湯浅能史（産業技術総合研究所）
- 概要
本チュートリアルでは、形式的体系を符号化し、定理証明支援系によって実現するための基本的な手法を解説する。例として、Martin-Loef型理論に基づく定理証明支援系Agdaをとりあげ、これによってホア論理の符号化を行い、その健全性の証明を実行する。Agdaについてもホア論理についても、特段の予備知識を仮定しない。ホア論理を知っている読者にとっては、Agdaによる符号化の解説になり、Agdaを知っている読者にとっても、ホア論理の解説になるよう試みる。
資料は以下のリンクからダウンロードしてください．(2006.11.01更新)
田辺のホーム