プログラム (ALGI 2015)

最終更新日時: Last modified: 2015-09-01

13:45 ～ 14:00

オープニング＋連絡など

14:00 ～ 14:30

安部 達也（理化学研究所）

演題：メモリ一貫性モデルを考慮したソフトウェアモデル検査のためのモデル検査器生成器 McSPIN

梗概：

プログラム検証方法の一つであるソフトウェアモデル検査が返す検査結果は、 その検査をどのメモリ一貫性モデル下で行うかにより一般に異なる。講演者が開発している モデル検査器生成器 McSPIN は形式化されたメモリ一貫性モデルを入力にとることで、例えば、 同一のプログラムに対する異なるメモリ一貫性モデル下での検査を簡単に行う方法を提供する。 本講演では、メモリ一貫性モデルを考慮したソフトウェアモデル検査を概説した上で、 McSPIN の仕様と実装を紹介する。また、メモリ一貫性モデルにより挙動を変えるプログラムを例にとり McSPIN の使用方法も紹介する。

14:30 ～ 15:00

西村 進（京都大学）

演題：順序複体上の連続変形発見による分散プログラムの導出

梗概：

組合せ幾何的手法による分散プログラムの計算構造の解析によって、 分散プログラムの実現不可能性についてこれまで多くの重要な結果が示されてきている。 本講演では、分散計算の幾何的記述からプログラムを導出することを目的とする。 これは一般には計算不可能な問題であり、導出アルゴリズムは完全とはなりえないので、 健全なものを得ることを目指す。このようなアルゴリズムは、幾何的記述から導かれる 順序複体上で連続変形を発見するための手続きとして実現できることを示す。

15:00 ～ 15:15 休憩

15:15 ～ 15:45

春山 栞（奈良女子大学）（共著者 鴨浩靖、酒井千尋、萩尾由貴子）

演題：ユークリッド幾何の問題への数式処理システムの応用

梗概：

計算代数学と数式処理技術の発達により、これまでは計算できなかった 複雑な数式も扱えるようになった。私たちは、近藤・齋藤・竹島の線形写像法を用いて、 平面ユークリッド幾何における最大最小問題の計算をできるだけ自動的に行うことを 目標としている。現在、いくつかの個別の問題に適用して、具体例の集積を行っている。 本講演では、その現状を報告する。

15:45 ～ 16:15

西田 美幸（奈良女子大学）（共著者 大和田菜摘）

演題：証明図エディタの作成

梗概：

記号論理学では証明図を使用する場面が多くあるが、 それらは記号入力や位置調整の問題で作成に手間がかかるものである。 私たちは証明図をより簡便に作成できる証明図エディタを開発する。 開発にはJava言語を用い、LaTeXでの使用を目的としている。 今回は先行研究を踏まえて実装する予定の機能を説明し、 開発中の証明図エディタで実装済み機能のデモンストレーションを行う。

16:15 ～ 16:30 休憩

16:30 ～ 17:00

河野 友亮（東京工業大学）

演題：最小量子論理の特殊な含意とカット除去定理について

梗概：

量子論理のシークエント計算の一つに、GO（西村1980）があるが、 カット除去が成り立たない系であった。今回はこの系に特殊な含意を加え、 さらにカット除去定理を成り立たせるために、ラベル付シークエントを導入する。

17:00 ～ 17:30

上村 太一（京都大学）

演題：Fibered Fibration Categories

梗概：

As a model of Homotopy type theory, Shulman introduced type theoretic fibration categories. We show that, for a fibred category whose base category is a type theoretic fibration category, fibrewise and total structures of type theoretic fibration categories coincide.

18:30 ～

懇親会（鳥取駅周辺 すし銀） 懇親会への参加を希望される方は、8/27（木）までに西澤 (nishizawa AT kanagawa-u.ac.jp) に メールでお知らせください。

10:00 ～ 10:30

蔵岡 誉司（国立米子工業高等専門学校）

演題：ファジィ代数上の１階述語論理式 - Subdirect productの視点から

梗概：

代数 $A$に対してファジィ代数$FS(A)$を定義 すると、それは束構造が付加された代数であり、$FS(A)$ は$A$のべき集合のSubdirect productとみなすことがで きる。この視点から、$A$上で成り立つ論理式と$FS(A)$ 上で成り立つ論理式を考察する。

10:30 ～ 11:00

田中 康平（信州大学）

演題：Discrete Euler integration and sensor networks

梗概：

空間のオイラー標数を測度と考え，ルベーグ積分のアナロジーとして， 関数の積分を行う操作をオイラー積分と呼ぶ。 Ghristらはこの積分を用いて，ある領域内に散らばるターゲットをセンサーにより数え上げる理論を確立した。 一方で，オイラー標数は幾何学的な対象だけでなく，離散的・組合せ論的な順序集合などにも定義されている。 本公演では，この離散的オイラー標数を用いた オイラー積分，およびその応用として， ネットワークに散らばるターゲットの数え上げの理論について解説したい。

11:00 ～ 11:15

クロージング＋連絡など