抽象化の技法2000


1 自動証明の参考文献

数理論理学(林晋著、コロナ社)

2 冠頭標準形と恒真性判定

まとめ

3 形式的技法の参考文献

ソフトウエア仕様記述の先進技法ーZ言語(ポター等著、田中訳、トッパン)

4 形式的仕様記述言語Zについて

99年度八杉特研卒業研究論文 (岩瀬、大西、平井、平田)
興味のある人は知らせてください。

5 プログラム検証論(林晋著 共立出版)

98年度八杉特研卒業研究論文 (布施田敏樹)


99年度期末試験問題と解答


10月31日まで:冠頭標準形とワンのアルゴリズムによる述語論理の自動証明;
ソフトウエア仕様記述言語Z(その意義、集合の記法、とくに論理式による記法)

11月21日:Zの表記法、というに関係の記法
スキーマの説明(図書館管理)

注:11月28日は10号館で!



11月28日:C2教室でZ言語の論文を読む

レポート課題! 問題用紙受け取っていない人は来週申し出てください。
提出日は用紙に書いてあります。提出は理学部事務室。大学指定の表紙をつけること
病気そのほかの理由で提出不可能の場合は必ず証明書持参で、八杉まで(後日で可)
申し出てください。



12月5日まででZ言語の基本はおわりました。
次回からはプログラム検証論の話をします。


期末試験について:99年度の問題と解答がおいてあるので、参考にしてください。

Z言語による記述、簡単なスキーマの作成、プログラム検証論における
部分正当性と完全正当性の記述(5ー6行)、それぞれ1題です。
最後の問題はあらかじめ解答を用意しておくこと。


12月19日:プログラム検証論とは、部分正当性と完全正当性、
ホーア論理、表明付きプログラム

    


新世紀明けましておめでとうございます

レポートの採点結果について
冠頭標準形とZ言語にすいてのごく基本的な問題でした。
基本的にはほとんどの人が理解していることがわかりました。
30点満点も多くありました。幸い15点を切った人はありません。
20点未満の人は「集合と論理」で習った分解の木(ワンのアルゴリズム)
を忘れたのでしょうか?テキストみればすぐわかるのに!
成績の一覧表を見せます。その後で要望に応じてレポートを貸しますが、
25点以上の方はご遠慮くだださい。
後で正解を貼っておきます。

レポート解答


1月16日まで:部分正当性の証明のためのHoare論理、PHL、の解説、
gcdのプログラムの部分正当性証明の一部分の解説
完全正当性のためのHoare論理、THL、の解説(違いはwhile文のみ)
詳細は参考資料5または6にあります。
なお、最後の週にはクイズを出すので、出席すること


1月23日:自然数上の「計算可能な関数」(再帰的関数)の定義(情報系数学入門の 73ページ)
英語でパズル:帽子の色あてパズル(答と理由を書いてもらいました。出席者 全員に数点追加)
多くの人が大体正しい理由を書いていました。念のために簡単に書いておきます。
以下はBiancaの推論です。「もし私の帽子が白でなかったら、少なくとも一方は
白なのだから、Annaは自分の帽子は白のはずだ、と分かったであろう。
でもAnnaは分からない、と答えた。と、いうことは、私の帽子は 白のはずである」
ということで、Biancaは自分の帽子は白である、ということを知る。
したがって「はい、私の帽子の色が白であることを知っています (分かります)」と答える。

ところで、これは論理的に推論しているのですが、今までに習った命題論理やbr> 述語論理ではできません。そもそも「知っている」とか「分かる」とか
いうことを表現するには新しい結合子みたいなものを導入しなければ
なりません。"Xであることを知っている"を表現するのにたとえば"K(X)"と
書きます。"K"を「知識作用素」とよびます。Kはknowのkです。
知識作用素をもつような論理を知識論理と呼ぶことができますが、
古くから知られている「様相論理」というのがこの役目をします。
様相論理は最近人工知能理論などで重要になっています。


今日でこの講義も終わりました。教科書がなくてわかりにくかったことも, あるかもしれません。
異なるテーマをいくつか扱ったので、教科書を 指定できませんでした。卒業論文を参考にしてください。
全体の統一的なテーマは、論理を道具にしてプログラムを研究する、という プログラミングの科学です。
そういうつもりでもう一度講義の内容を 反復してください。
では期末試験の健闘を!


成績評価方法 レポート(満点30点)+パズル(提出者全員5点)+期末試験(満点70点) =105点;大学の基準にしたがって60点以上を合格とする。
幸か不幸か、合計点が100点を越えた人はいませんでした。
一人の例外を除いて、不合格になったのはレポートを提出しなかった人です。
レポートや中間試験を粗末にしないように気をつけましょう。

〇合否の結果は消去しました。 ../
/

Last modified: Thu Apr 8 14:32:52 JST 2004