数理システム特論

Advanced Mathematical Systems

997D303

74AIAPM501

秦野　亮

Ryo Hatano

2025年度後期

2025年度

②Second semester

月曜4限

Monday 4th Period

創域理工学研究科　経営システム工学専攻

Department of Industrial and Systems Engineering, Graduate School of Science and Technology

2.0単位

講義

Lecture

-

① [対面]対面授業/ [On-site] On-site class

計算機科学における論理を用いた形式化について学ぶ．数学の厳密な議論やヒトの日常における曖昧な思考など，捉えがたい対象をいかにして計算可能なシステムとして体系化し，人工知能システムへと活用するかについて概説する．

This course will offer formalization based on mathematical logic in computer science. It provides an overview of how to formalize elusive subjects that exist in our mind, such as rigorous mathematical arguments and ambiguous human thoughts, into computable systems and how to apply them to develop modern artificial intelligence systems.

計算機科学における重要な論理の基礎について理解し，真理計算や証明の方法論を習得する．
本専攻のディプロマ・ポリシー「経営システム工学専攻の専門分野に応じた高度な専門知識 」に該当する科目である.

This course aims to provide students with a better understanding of the foundation of mathematical logic in computer science and teach them methodologies for truth calculation and proof.
This course falls under the diploma policy "Advanced expertise according to the specialized field of the Department of Industrial and Systems Engineering."

人工知能システムを設計・開発するために重要な様々な技法を，論理を通して理解できるようになる．

Students are able to understand various important techniques for designing and developing artificial intelligence systems from a logical perspective.

リンク先の [評価項目と科目の対応一覧]から確認できます（学部対象）。
履修登録の際に参照ください。
​You can check this from “Correspondence table between grading items and subjects” by following the link(for departments).
https://www.tus.ac.jp/fd/ict_tusrubric/​​​

授業中に筆記用具・ノート及びノートパソコンを使用するので，必ず持参すること．

Bring your stationery and laptop.
Ensure the laptop is fully charged.

課題に対する作文　Essay／小テストの実施　Quiz type test／プレゼンテーション　Presentation

-

各回の授業内容を十分に復習しておくこと．

Review the contents of each class thoroughly.

授業を全て受けていることを前提とし，課題レポート・課題発表・演習などの結果によって成績を評価する．

Your grade is evaluated based on the results of assignment reports, assignment presentations, exercises, and other assignments, assuming you have taken all the classes.

・S：到達目標を十分に達成し、極めて優秀な成果を収めている
・A：到達目標を十分に達成している
・B：到達目標を達成している
・C：到達目標を最低限達成している
・D：到達目標を達成していない
・-：学修成果の評価を判断する要件を欠格している

・S：Achieved outcomes, excellent result
・A：Achieved outcomes, good result
・B：Achieved outcomes
・C：Minimally achieved outcomes
・D：Did not achieve outcomes
・-：Failed to meet even the minimal requirements for evaluation

N

-

教科書および一部の参考書は、MyKiTS (教科書販売サイト) から検索・購入可能です。
​https://gomykits.kinokuniya.co.jp/tokyorika/​​​

It is possible to search for and purchase textbooks and certain reference materials at MyKiTS (online textbook store).
​​https://gomykits.kinokuniya.co.jp/tokyorika/

小野寛晰, 情報科学における論理 (情報数学セミナー), 日本評論社, 1994.
鹿島亮, コンピュータサイエンスにおける様相論理, 森北出版, 2022.
菊池 誠, 佐野 勝彦, 倉橋 太志, 薄葉 季路, 黒川 英徳, 数学における証明と真理: 様相論理と数学基礎論, 共立出版, 2016.
Patrick Blackburn, Maarten de Rijke and Yde Venema, Modal Logic, Cambridge University Press, 2002.
David Harel, Dexter Kozen and Jerzy Tiuryn, Dynamic Logic, MIT Press, 2000.

1. ガイダンス
　　論理による形式化について概要を理解する.

2〜4. 命題論理に基づく形式化
　　意味論・証明論について基本的な考え方を理解する．

5〜7. 述語論理に基づく形式化
　　命題論理では捉えられない対象を述語論理に基づいて捉える方法について学ぶ．

8〜9. 述語論理の応用
　　述語論理を応用した論理プログラミングについて学ぶ．

10~12. (多) 様相論理に基づく形式化
　　可能・必然の分析に基づく様々な様相を論理で捉える方法について学ぶ．

13〜. より発展的な話題
　　定理証明支援系などより発展的な話題について学ぶ．

※全ての講義を対面で受講することを求める.

1. Guidance
    To understand an overview of logical formalization.

2-4. Formalization (Propositional logic)
    To understand the methodology of semantics and proof theory on propositional logic.

5-7. Formalization (First-order predicate logic)
    To understand the method for capturing subjects that cannot be expressed in propositional logic based on First-order predicate logic.

8-9. Logic Programming (First-order predicate logic)
    To understand the methodology of Logic Programming based on First-order predicate logic.

10-12. Formalization (Modal logic)
     To understand how to capture various modalities by analyzing possibility and necessity using modal logic and their extension.

13-. Advanced topics
    To understand more advanced topics such as a formal proof management system.

※All classes are held in person.

-

-

-SWI-prolog
-Coq Proof Assistant

Y

N