Основні поняття
本論文では、二変数論理式FO2にPresburger算術の量化子を追加した拡張論理式FO2Presの満足可能性と有限満足可能性が決定可能であることを示す。また、任意のFO2Pres文の有限モデルの大きさの集合(スペクトラム)がPresburger算術で定義可能であることを示す。
Анотація
本論文では、二変数論理式FO2にPresburger算術の量化子を追加した拡張論理式FO2Presについて研究を行っている。
主な内容は以下の通り:
-
FO2Presの満足可能性と有限満足可能性が決定可能であることを示した。
- FO2Presは、FO2に最終的に周期的な集合に関する量化子を追加したものである。
- 従来の研究では、FO2の拡張であるC2の満足可能性と有限満足可能性が決定可能であることが知られていた。
- 本論文では、FO2Presの満足可能性と有限満足可能性も決定可能であることを示した。
-
FO2Pres文の有限モデルの大きさの集合(スペクトラム)がPresburger算術で定義可能であることを示した。
- スペクトラムとは、ある論理式を満たすモデルの大きさの集合のことである。
- 先行研究では、C2の場合のスペクトラムがPresburger算術で定義可能であることが示されていた。
- 本論文では、FO2Presの場合のスペクトラムもPresburger算術で定義可能であることを示した。
-
証明の過程で、制約付き二部正則グラフの問題に関する新しい結果を示した。
- 二部正則グラフの制約付き問題を解くことで、FO2Presの満足可能性と有限満足可能性の決定可能性を示した。
- 制約付き二部正則グラフの問題に関する新しい結果として、グラフの partition サイズの集合がPresburger算術で定義可能であることを示した。
全体として、本論文は二変数論理式の拡張であるFO2Presの重要な性質を明らかにしたものであり、論理学と計算理論の分野に貢献するものである。
Статистика
以下のような重要な数値が論文中に登場する:
最終的に周期的な集合(u.p.s.)の表現には、オフセットと周期の情報が含まれる。
FO2Presの式では、最大のオフセットを q と表している。
良い振る舞い関数(good behavior)の値域は、{0, ..., q, 0+p, ..., q+p, ∞}の範囲に限定される。
Цитати
以下のような重要な引用が論文中に登場する:
"We consider the extension of FO2 with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set."
"We show that both satisfiability and finite satisfiability of the logic are decidable."
"We also show that the spectrum of any sentence, i.e., the set of the sizes of its finite models, is definable in Presburger arithmetic."