新着情報
カテゴリ:大学院集中講義
教育研究科 集中講義（12月3日〜5日）
terui
科目番号：01B6641
科目名：数学特論I
日時：2014年12月3日（12:15開始）、12月4日、12月5日（4日と5日の日程は3日に連絡します）
場所：自然系学系棟 D814
担当教員：岩根 秀直先生（国立情報学研究所）
講義題目：計算代数における実閉体上の限量記号消去法
科目名：数学特論I
日時：2014年12月3日（12:15開始）、12月4日、12月5日（4日と5日の日程は3日に連絡します）
場所：自然系学系棟 D814
担当教員：岩根 秀直先生（国立情報学研究所）
講義題目：計算代数における実閉体上の限量記号消去法
講義概要：
限量記号消去法 (Quantifier Elimination: QE) は, 限量記号がついた一階述語論理式を入力として，それと等価で限量記号のない論理式を出力するアルゴリズムである．一階述語論理式の記述力能力は高く, 制御・最適化など多くの応用をもち, QE は非常に重要である.
実閉体上での QE アルゴリズムについては, 1930 年に A. Tarski がその存在を示し, 具体的なアルゴリズムも示した. 現在では, より効率的な汎用 QE アルゴリズム Cylindrical AlgebraicDecomposition のほか, 特別な問題のクラスに対するより効率的な QE アルゴリズムの研究がすすめられている.
本講義では, QE を実現するために必要な計算代数の基礎知識, QE アルゴリズム, QE ツールの利用方法, QE の効率的な実装方法, および, 実問題への適用方法について紹介する.
本講義は, 主に穴井・横山著「QE の計算アルゴリズムとその応用」の内容を補完する形で進めるが, その内容を前提としない予定である.
備考：
限量記号消去法 (Quantifier Elimination: QE) は, 限量記号がついた一階述語論理式を入力として，それと等価で限量記号のない論理式を出力するアルゴリズムである．一階述語論理式の記述力能力は高く, 制御・最適化など多くの応用をもち, QE は非常に重要である.
実閉体上での QE アルゴリズムについては, 1930 年に A. Tarski がその存在を示し, 具体的なアルゴリズムも示した. 現在では, より効率的な汎用 QE アルゴリズム Cylindrical AlgebraicDecomposition のほか, 特別な問題のクラスに対するより効率的な QE アルゴリズムの研究がすすめられている.
本講義では, QE を実現するために必要な計算代数の基礎知識, QE アルゴリズム, QE ツールの利用方法, QE の効率的な実装方法, および, 実問題への適用方法について紹介する.
本講義は, 主に穴井・横山著「QE の計算アルゴリズムとその応用」の内容を補完する形で進めるが, その内容を前提としない予定である.
備考：
- 全学計算機（サテライト）端末を用いた実習を予定しているので、履修者は全学計算機のアカウントを確認しておくこと。
- 本講義は教育研究科の授業科目ですが、他研究科の学生も単位を修得できる場合があります。詳細は各専攻事務室へ相談してください。
世話人：照井 章（数理物質系 数学域）
