fc2ブログ

Entries

ダニエル・フリードマン、カール・イーストルンド『定理証明手習い』

Lisp/Scheme言語での定理証明支援形ACL2をモチーフにして、証明の形式化について平易に扱ったもの。全編、対話形式で書かれている。読みやすくはあるが、その分ポイントが流れて行ってしまい、分かりにくさも感じる。


主にリストを使った操作について、帰納法的証明を形式的に行うのをゴールにしている。リストのサイズや、リスト内の一で重みづけたスコアを帰納法のインデックスとして、帰納法が停止すること、よって全域関数になることを示していく。ただ話はあくまでLisp/Schemeの特定の言語体系での形式証明の初歩的紹介なので、そもそも定理自動証明とは何かについて知られる本ではない。ちょっと読む本を間違えた。

スポンサーサイト



この記事にトラックバックする(FC2ブログユーザー)
https://exphenomenologist.blog.fc2.com/tb.php/1416-6bffc2ad

トラックバック

コメント

コメントの投稿

コメントの投稿
管理者にだけ表示を許可する

Appendix

プロフィール

坂間 毅 (Sakama Tsuyoshi)

Author:坂間 毅 (Sakama Tsuyoshi)
コンサルティングファームに所属。数学の哲学を専攻して研究者を目指し、20代のほとんどを大学院で長々と過ごす。しかし博士号は取らず進路変更。以降IT業界に住んでいる。

別館:note

検索フォーム

QRコード

QRコード