第20回「記号論理学と情報科学」 アブストラクト

Modal logics for coalgebras (survey), 蓮尾　一郎(東工大)

The notion of coalgebra is an abstraction of state-based systems such as automata and Kripke models. Modal logic has proved to be useful as a specification language for behaviors of coalgebras. There are some different approaches taken by different authors; the aim of this presentation is to give a brief overview of them.

Regular category の中の非決定性オートマトン, 池上 大介(産総研/CREST)

非決定性オートマトンから、受理言語が等しい決定性オートマトンを変換すること ができる。しかし、変換されたオートマトンの状態数は変換前に比べて指数的に 増大するのが問題である。そこで、非決定性オートマトンを(決定性オートマトンに 変換せずに)扱うことができれば望ましい。一方、受理言語が等しい非決定性オートマトン は沢山あるので、その中から「扱いやすい非決定性オートマトンとは何か」を決める 必要がある。本発表では、非決定性オートマトンを regular category で再定義し、 非決定性オートマトンの“最小化”を考察する。決定性オートマトンから決定性 オートマトンへの状態写像(*1)は、受理言語が等しい決定性オートマトン同士の順序を 定義する。その順序のもとで最小の決定性オートマトンを最小オートマトンと呼ぶ (*1: S. Eilenberg, “Automata, Languages, and Machines”)。本発表では、 Eilenberg の状態写像を非決定性オートマトンに拡張し、非決定性オートマトンの 最小化を拡張された状態写像で定義する。

抽象解釈にみられる圏論的構成について, 西澤 弘毅(東大/産総研)

Cousotらによる抽象解釈の理論において暗黙的に 用いられている圏論的な構成をいくつか明示し、 より広い応用のための基礎を与えることを試みる。

明示的代入計算の強正規化性の証明について, 桜井貴文(千葉大)

明示的代入計算 λx で型付け可能であれば強正規化可能であるこ との証明はいくつか知られているが、本講演ではより従来のものより簡単な証 明を与える。

様相μ計算の完全性について, 鹿島 亮(東工大)

様相μ計算のシンプルな公理系が完全であることを，Walukiewicz による難解 な証明とはまったく別な方法で簡潔に証明することを目標とする．現在は目標 の半分程度（？）まで到達している．

Flow Analytic Type System for Compiler Optimizations , 松野裕(東大)

コンパイラ最適化の正しさの証明を型理論の枠組みを用いて行う。

NP完全問題を解く決定性アルゴリズムについて, 久馬栄道(愛知学院大)

決定問題は、答として"yes"か"no"だけがわかればよいが、 一般のコンピュータは構成的数学で動いているので、それ以上の 情報がわかってしまう。 そこでここでは、そのようなことのないようなNP完全問題を 解く決定性アルゴリズムを考える。

On Sufficient Conditions And Partial Analysis for Secure Cryptographic Protocols, Masao Mori (九大)

On the model by Dolev and Yao we represent a sufficient condition, called name-suffixing, and give its proof in order to design secure single message protocols, namely ping-pong protocols. This condition is simply to insert identities of participants in messages. The similar our result has been found by Lowe who points out a vulnerability of the Needham-Schroeder protocol and gives its correction. That is essentially to include participants identities in messages. We introduce an extension of free monoid of protocol-operation which is given as a= simple term rewriting system. The extension for plural messages consists of multiplexing duplicate messages. Firstly we will focus on the case of duplicate messages. The term rewriting system is used such as the corruption rule in the case of single message. On that system the algorithm by Dolev et al. for duplicate message is discussed. To support the case of plural messages, algorithms should be combined in an appropriate way. In addition, a sufficient condition is discussed to construct secure cryptographic protocols. This condition is extended version of name-insertion property.

情報と依存関係の論理 , 小林 聡(京産大)

「x の値がわかる」を意味するような1項の述語D(x)と、non-informative な quantifier を持つ論理を考える。今回与える公理系は、一見古典論理に反す るように見えるが、実は自然なものであって、証明論的・意味論的に良い性質 を持っている。

The double-negation and ?! translations of classical logic, 白旗　優(慶應大)

Classical logic can be translated either into intuitionistic logic by the double-negation translation or into linear logic by the ?! translation. We compare them in terms of Dialectica-style interpretations of intuitionistic and linear logics.

等式の対応関係について, 西原 秀明(産総研/CREST)

等号を持つ論理体系を複数考え、それぞれの等式の対応関係を 考察する。特に多対一対応するものなど、複雑な例をいくつか あげたい。

SLACS2003プログラムに戻る