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

プログラム

2004年9月9日（木）〜10日（金）

９月９日午前

フーリエ変換を用いたSATの解法, 久馬栄道（愛知学院大学教養部）

NP完全問題は、非決定性アルゴリズムで特徴づけられる。 しかしながら、SATを解くときなどを分析すると、非決定性を有効に使っていないように 思われる。
また、NP完全問題は決定問題であるので、答として"yes"と"no"だけがわかれば良いが、 通常のアルゴリズムは、構成的数学の上で動いているので、解く過程で"yes"と"no"以外の余分な情報がわかってしまう。
ここでは、決定性でなおかつ余分な情報がわからないような、SATを解くアルゴリズムを考察する。 また、その一例として、フーリエ変換をもちいたSATの解法を考える。

擬コンパクト空間におけるDiniの定理の計算可能性版について, 鴨浩靖（奈良女子大学理学部情報科学科）

擬コンパクト距離空間への計算可能性構造の入れ方を複数提案し、 その一つでDiniの定理の計算可能性版が成り立つことを示す。
一般にDiniの定理として知られているのはコンパクト空間上でのも のだが、擬コンパクト空間においても同様の定理が成り立つことが すでに知られている。一方、空間のコンパクト性を実効的コンパク ト性に置き換え、関数の連続性を計算可能性に置き換えた、Diniの 定理の計算可能性版と呼べる定理が、実効的コンパクト距離空間に 限定された形ではあるが、講演者によってすでに証明されている。 そこで、本講演では、擬コンパクト空間におけるDiniの定理につい て、同様に計算可能性版が成り立つか、考察を行う。

情報と依存関係の論理, 小林 聡 （京都産業大学理学部コンピュータ科学科）

「x の値を知っている」を意味する述語D(x)を持ち、情報の隠蔽や情報 間の依存関係を詳細に記述できる論理を提案する。昨年の発表内容に比べ、 公理系、意味論共により自然なものに改良した。今回は主に体系の形式的 性質について述べるつもりである。

９月９日午後

Strong Normalizability of Calculus of Explicit Substitutions, 桜井貴文(千葉大)

明示的代入計算λxに加えても強正規化性が成り立つような合成規則について は、BlooとGeuversによる研究が知られている。本講演では、彼らの合成規則 とは異なる合成規則で、λxに加えても強正規化性が成り立つ規則を与える。

近似様相と不動点演算子, 中野 浩（龍谷大学 理工学部）

負の自己参照を矛盾なく取り扱うために考案された近似様相付 きの型付けシステムでは、Curry や Turing の不動点演算子に 対して、その型情報のみを用いて再帰的なプログラムが構築可 能となるような型を与えることができる。 本講演では、連続 λモデルにおいて、ある元がこの型を持つことと、最小不動点 演算子であることとが同値となることを紹介する

様相論理S4における1変数の論理式について, 佐々木克巳（南山大学数理情報学部）

本報告では、命題変数pから∧(論理積),∨(論理和),⊃(含意),□(必然) を用いて構成される様相論理の論理式の集合S(p)を対象とする。そして、順序集合 の構造を明らかにする。ただし、≡は様相論理S4での証明可能性を法 とする同値関係、≦はS4での導出関係、すなわち 　　[A]≦[B]　⇔　あるA'∈[A]とB'∈[B]に対して、A'⊃B'がS4で証明可能 である。この順序集合は、既にブール代数であることが知られているが、ここでは、 その同値類の代表元を帰納的に構成することで、そのより詳細な構造を明らかにする。

証人の論理―伝聞を表す様相述語論理, 竹内泉（東邦大学理学部）

様相記号が「彼はこう言った」を意味するような様相述語論理に ついての研究を発表する。ここで問題となるのは、共有する個体領 域と各主体に独立の個体領域と両方を扱うことの困難である。

General frames for relevant modal logics, 関隆宏（九州大学　大学評価情報室）

古典様相論理では Kripke frame と様相代数を組み合わせた general frame がしばしば用いられる。本講演では、適切様相 論理に対する general frame を新たに導入し、古典様相論理 に対する general frame と同様な性質が成り立つことを示す。

Gentzen Style Sequent Calculi for Logics with Strict Implication and Weak Logics , 石垣 良（東京工業大学 情報理工学研究科 ）

厳密含意とは古典論理に於ける実質含意とは異なる含意である. 厳密含意は様相論理の研究に於いて重要な役割を果たした. 様相論理に於いて厳密含意は必然的な含意として解釈される. 本発表は厳密含意を持つ非様相論理について考える. 厳密含意と実質含意の両方を持つ論理を厳密含意を持つ論理と呼び, 厳密含意のみを持つ論理を弱い論理と呼ぶ. 私達は主な15個のクリプキモデルに よって特徴付けられる厳密含意を持つ論理と弱い論理の為のシーケント計算を導入し, 完全性定理を証明する.

９月１０日午前

量子論理と束論, 山下秀康（愛知学院大学教養部 ）

なし

高階論理の完全性とその周辺について, 岡本圭史（産業技術総合研究所）

高階論理の標準的モデルに対する完全性は、ゲーデルの不完全性定理 により、成り立たないことが知られている。ここでは、モデルに関す る条件を弱めた、一般的モデルというクラスを新たに定義し、このク ラスに対しては完全性が成り立つという、ヘンキンの結果を紹介する さらに、その周辺の事柄についても紹介する。
An extension of Chaitin's halting probability \Omega to measurement operator in infinite dimensional quantum system, 只木孝太郎 （中央大学21世紀COEプログラム)

We propose an extension of Chaitin's halting probability \Omega to measurement operator in infinite dimensional quantum system. Chaitin's \Omega is defined as the probability that the universal self-delimiting Turing machine U halts, and plays a central role in the development of algorithmic information theory. In the theory, there are two equivalent ways to define the program-size complexity H(s) of a given finite binary string s. In the standard way, H(s) is defined as the length of the shortest input string for U to output s. In the other way, the so-called universal probability m is introduced first, and then H(s) is defined as -log_2 m(s) without reference to the concept of program-size.
Mathematically, the statistics of outcomes in a quantum measurement are described by a positive operator-valued measure (POVM) in the most general setting. Based on the theory of computability structures on a Banach space developed by Pour-El and Richards, we extend the universal probability to an analogue of POVM in infinite dimensional quantum system, called universal semi-POVM. We also give another characterization of Chaitin's \Omega numbers by universal probabilities. Then, based on this characterization, we propose to define an extension of \Omega as a sum of the POVM elements of a universal semi-POVM. The validity of the definition is discussed.

SLACS2004プログラムに戻る