ゲームプログラマのための数学の歩き方～様相論理編～
受講スキル
数学が得意でなくても、数学を知りたい方。 数学に関する前提知識は不要ですが、講演内の一部、具体的な解説を行う部分に関しては、基本的な命題論理を知っていると理解しやすいかもしれません。
受講者が得られるであろう知見
プログラムの検証の背景にある数理論理学を理解できます。 また、こうした学習を独力で行うためのロードマップを知ることができます。
セッションの内容
※ 本講演は、CEDEC2020～CEDEC2022講演『ゲームプログラマのための数学の歩き方』の続編ですが、内容につながりはありません。独立してご聴講いただけます。
近年ゲーム開発におけるQAコストは大幅に増加しています。
この課題に対する一つの解決策として、プログラムの検証が挙げられます。
例えば、C++では「契約プログラミング」による検証のための仕様追加が検討されています。
また形式手法を利用したソフトウェアの形式検証をゲーム開発に応用する事例も増えてくるかもしれません。
本講演では、こうしたプログラムの検証で必要となる、ホーア論理や様相論理といった数理論理学の入口や大まかな全体像の把握を目指します。
昨年度講演同様、独力で学ぶための参考にしていただければ幸いです。
講演資料
※資料のダウンロードには ログイン が必要です。
講演者プロフィール
プロフィール
オープンソース開発、ソフトウェアプロダクト開発、エンタープライズシステム開発などの様々な開発を経てゲームプログラマに。株式会社スクウェア・エニックスでは、Luminous Studio、FINAL FANTASY XVの開発に参加し、VFX・UIを担当。産学連携による共同研究の仕組み作りに従事し、2022年より現職。専門は言語処理系。ACM SIGGRAPH Asia 2018 Real Time Live! Chair、2021 Games Chair。共著『ゲームエンジニア養成読本』（Software Design plusシリーズ、技術評論社）。
《講演者からのメッセージ》
毎年書いている気がしますが、独力で数学を学ぶのって難しいですよね。
今年は少し方向性を変えてみましたが、これまで同様、高校数学と大学数学の壁を越える一助になれば幸いです。
プロフィール
2004年、大阪大学 大学院基礎工学研究科 博士課程を修了。同年、岡山県立大学 情報工学部 助手。2016年、同大学 情報工学部 准教授。博士（工学）。専門分野はモデル検査を用いたソフトウェアシステムの形式的検証。情報処理学会主催のソフトウェアエンジニアリングシンポジウム（2013〜2022）およびウィンターワークショップ（2014〜2023）において、形式手法の情報交換を目的としたセッションを開催。過去の講演として、「形式仕様記述を用いたモデルベースのソフトウェア検証技術」（ベリサーブ アカデミック イニシアティブ 2016）など。
《講演者からのメッセージ》
ホーア論理や様相論理など、普段のゲーム開発ではあまり意識しない数理論理学の内容を扱いますが、多くの方の参考となるような講義にしたいと思います。
共同研究・開発者
鍛冶 静雄 (九州大学)
落合 啓之 (九州大学)
溝口 佳寛 (九州大学)