渕一博記念コロキウム『論理と推論技術:四半世紀の展開』

ちょうど僕の研究室のボスが代表を務めていたので行ってきました。
前提知識のない僕には難しい話も多かったですが(KL1すらよく知らない)、知らないなりにも単語だけはメモって来ました。自分の研究の方向性の今回のことでだんだん見えてきたりしたのでいってよかったです。いや、それにしても人の名前マイクで呼ばないで!!

以下メモ。

《基調講演》『渕一博の思想:なぜ論理だったのか?』 林 晋

始まる時間が僕には早すぎました。確信的に聞き逃した。

『非単調性と帰納論理を取り入れたことで論理プログラミングはどう変わったか?』

内容はあまりわからなかった。推論技術の発展の話? とりあえず、出てきた単語メモ。
Abduction,Induction,Deduction, このへん? -> http://en.wikipedia.org/wiki/Logical_reasoning
SOL resolution, disjunctive program, non monotonic, Inverse Entailment for induction, alaboration tolerance,

Algorithm = Logic + Control (Kowaiski)

『記号的統計モデリングの世界を探る』 佐藤 泰介

論理と統計的手法を組み合わせる話。現実に多くある決定的でない事象に対して論理を適用するにはこのような手法は重要に感じます。自然言語の解析が例として話で出てきていました。
この方の話で、どうゆう文脈で出てきたかは覚えていませんが、変数同士の依存関係が変数の特定の値の依存関係であることが多いので、値同士の依存関係を使ったほうが依存関係が絞れるというようなことを言っていました。

帰納・発想論理プログラミングとスキルサイエンス』古川 康一

帰納(inducti)論理、発想(abductive)論理は演繹論理とは方向が逆で、結果とルールからデータを求めたり、結果と入力からルールを求めたりするらしい。

『モデル生成型定理証明系MGTPの要素技術』長谷川 隆三

充足可能性問題をSATソルバよりも効率的に解ける場合があるとのこと。SATに力を入れているボスとしては気になったようで、「我々としては確かめなければ」と後で言っていた。

『非数値並列計算の動向と展望』中島 浩

おもしろかったのが、数値計算の世界ではおばかな並列化でも結構受けるという話。CSの世界では難しい並列化をしないと受けないのだそうです。 それから、どのような文脈かは思い出せませんが、並行と並列の美的な融合が最難間だった、という話がありました。平行性がプログラミング言語や処理内容にあったとしても、並列化するのは自明ではないということか。
それから、並列化のこれからのはなし。予想。

  • 1Pの性能向上は止まる! -> 並列しかない!
  • 逐次性の打破は投機!
  • 結果の非決定性は恐れずに受け入れる!(並列論理型言語に対して)
  • 10^6Pを恐れない!

『ゲノムと論理:論理推論はバイオインフォマティクスを超えられるか?』小長谷 明彦

複数の薬の依存関係を論理で推論するという話。
話の後で近山先生が、記号処理できるように対象を抽象化して処理をして、シミュレーションすべき部分(記号処理できない部分)を見つけられるだろうということをいっていました。こうすると処理が高速にもなる。

『21世紀のチューリングマシン ― 多様化した計算概念の統合』上田 和紀

ノイマン型計算機の上で20世紀に主に使われた計算モデルである、チューリングマシン、ラムダ計算などはもう古い。21世紀になっての、multi-core,クラスタ、グリッド、分散、組み込みなどさまざまなプラットフォームの上での計算に適したモデルはなんだろう。-> 今のところ知識と並列性を結びつけた、論理、並列論理プログラミングだ。 という話でした。それから、論理や制約プログラミングの歴史についての話もありました。

さすがにうちのボスの話なのでもう聞いた話も多かったけれども、先生がどのようなことを考えているかを改めて確認できた。さまざまな計算モデルの統合とさまざまなプラットフォーム上での動作を目標としたプログラミング言語の開発。いやはや先生の目標は高い。

『制約に基づく言語処理から制約なしの言語処理へ』 松本 裕治

『分散制約推論:マルチエージェントシステムの基盤技術』 横尾 真

マルチエージェントのアルゴリズムって理論的にやろうとすると難しそうです。