授業科目名	数理と論理に基づく情報処理
時間割番号	TCS328
担当教員名	岩沼　宏治
開講学期・曜日・時限	前期・火・IV	単位数	2
＜対象学生＞
(未登録)
＜授業の目的＞
数理論理や数理科学に基づく，プログラムやハードウエアの仕様記述，開発と検証法に関する理論と技術について学ぶ。これらは極めて高い信頼性を必要とする大規模システム（例えば CPU，分散並列サーバーシステム，ICカードや自動車などへの組み込みシステムなど）を開発する際の基礎をなす技術である．具体的には，情報処理学会J07-CSの「離散構造」及びJ07-SEの「論理と計算理論」ならびに「形式手法」の項目に準拠し、その一部を取り上げる．
＜本授業科目による獲得・涵養が特に期待されるコンピテンシー＞（能力・資質）
工学部(～2023年度入学生)>コンピュータ理工学科向け 記号 コンピテンシー（能力・資質）   CS-A 専門 5.時代の変化に対応できるよう、最新の技術動向を考慮して、自律的・継続的に学習できる。 ◎ CS-B 6.情報科学、及び、数学や自然科学等の知識と手法を用いて、以下のことができる。 6a.解決すべき問題を形式化することができる。 ○ CS-C 6b.要求、時間、費用、資源等の制約条件を考慮した上で、複数の解が存在するような複雑な問題の中から適切な解を見つけ出すことができ ○
＜到達目標＞  到達目標とは
目標NO 説明 コンピテンシーとの対応 CS 1 形式的手法の基盤となる数理論理やモデル検査法などの数理科学の基礎について説明できること CS-A 2 Floyd-Hoare論理や有限状態モデルなどに基づくシステムの記述と，正当性の検証に関する基本的事項を説明できること CS-B 3 幾つかの実例を通して，形式的仕様記述の実際について説明できること CS-C 4 NuSMVなどの形式的な仕様記述検証ツールを初歩的レベルで使用できること CS-C
＜成績評価の方法＞
目標No 割合 評価の観点 1 25% 数理科学の基礎の理解度 2 35% システムの記述と正当性の検証に関する基本的事項の理解度 3 15% 形式的仕様記述の実際に関する理解度 4 25% 形式的な仕様記述検証ツールの理解度と応用力 合計 100%
＜授業の方法＞
講義は面接授業を基本として，小テスト（オンライン型）を毎回行う． ・Moodle上に講義資料と復習用動画資料を公開し，オンデマンド型授業の長所を取り入れる． ・講義の後半において，プログラム理論の応用を理解するためにPC上で演習を行う ・成績評価は複数回のレポートと小テストにより行う．
＜受講に際して・学生へのメッセージ＞
離散数学（集合，順序，関係など），線形代数，アルゴリズムとデータ構造，プログラミング言語論，オートマトンと形式言語，オペレーティングシステムが前提知識と関連知識である．
＜テキスト＞
(未登録)
＜参考書＞
産業技術総合研究所システム検証研究センター, モデル検査初級編, 近代科学社, ISBN:9784764955059 藤倉俊幸, 組み込みソフトへの数理的アプローチ : 形式手法によるソフトウェアの仕様記述と検証, CQ出版, ISBN:9784789838085
＜授業計画の概要＞
1 タイトル ガイダンスと命題論理の基礎 事前学習 事後学習 事前配布の講義資料の予習と講義の小テスト 授業内容 命題論理式，標準形，モデル，充足可能性，判定手続き 2 タイトル SATソルバーの基礎 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 SAT決定問題，節形式，SATソルバー，DPLL手続き 3 タイトル 最新SATソルバーの実際その１ 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 単位伝番，矛盾からの節学習，学習節の評価 4 タイトル 最新SATソルバーの実際その２ 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 CDCLソルバー，変数選択戦略，制約充足問題 5 タイトル 述語論理の基礎 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 意味とモデル．充足可能性と恒真性 6 タイトル 述語論理の推論ー証明体系 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 記号操作に基づく意味推論：自然演繹法 7 タイトル プログラムの正当性 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 システムの正当性とは？：　事後条件、帰納表明 8 タイトル 構造化プログラミング 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 ダイクストラの構造化法，プログラム図式 9 タイトル プログラムのための論理：Hoare論理 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 プログラムの正当性検証のための形式体系 10 タイトル 計算可能性と計算量の理論 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 計算不可能性，ゲーデルの不完全性定理 11 タイトル モデル検査 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 時間論理とNuSMV 12 タイトル 演習その１ 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 NuSMVとモデル検査 13 タイトル 演習その２ 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 NuSMVとモデル検査（続き） 14 タイトル 演習その３ 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 NuSMVとモデル検査（続き） 15 タイトル 産業界における形式手法利用の実際 事前学習 事後学習 事前配布の講義資料の予習と講義後の小テスト 授業内容 VDM,　CCS，　時相論理 16 タイトル 事前学習 事後学習 授業内容 17 タイトル 事前学習 事後学習 授業内容 18 タイトル 事前学習 事後学習 授業内容 19 タイトル 事前学習 事後学習 授業内容 20 タイトル 事前学習 事後学習 授業内容 21 タイトル 事前学習 事後学習 授業内容 22 タイトル 事前学習 事後学習 授業内容 23 タイトル 事前学習 事後学習 授業内容 24 タイトル 事前学習 事後学習 授業内容 25 タイトル 事前学習 事後学習 授業内容 26 タイトル 事前学習 事後学習 授業内容 27 タイトル 事前学習 事後学習 授業内容 28 タイトル 事前学習 事後学習 授業内容 29 タイトル 事前学習 事後学習 授業内容 30 タイトル 事前学習 事後学習 授業内容
＜前年度授業に対する改善要望等への対応＞
前年度の授業アンケートにおいて，講義内容の周辺事項の解説について賛否両方の意見が寄せられた．今年度は試行として，周辺事項を少し減らし，講義での口頭説明の分量の削減を試みる予定である．その他は前年度と同様に実施する予定である．
＜備考＞
(未登録)